This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Axiom ax-2

Description: AxiomFrege. Axiom A2 of Margaris p. 49. One of the 3 axioms of propositional calculus. It "distributes" an antecedent over two consequents. This axiom was part of Frege's original system and is known asFrege in the literature; see Proposition 2 of Frege1879 p. 26. It is also proved as Theorem *2.77 of WhiteheadRussell p. 108. The other direction of this axiom also turns out to be true, as demonstrated by pm5.41 . (Contributed by NM, 30-Sep-1992)

		Ref	Expression
	Assertion	ax-2	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	1 2	wi	⊢ ( 𝜓 → 𝜒 )
4	0 3	wi	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
5	0 1	wi	⊢ ( 𝜑 → 𝜓 )
6	0 2	wi	⊢ ( 𝜑 → 𝜒 )
7	5 6	wi	⊢ ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) )
8	4 7	wi	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( ( 𝜑 → 𝜓 ) → ( 𝜑 → 𝜒 ) ) )