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	$$⊢\left(\phi \to \left(\psi \to \chi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \chi \right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	$$wff\phi$$
1		wps	$$wff\psi$$
2		wch	$$wff\chi$$
3	1 2	wi	$$wff\left(\psi \to \chi \right)$$
4	0 3	wi	$$wff\left(\phi \to \left(\psi \to \chi \right)\right)$$
5	0 1	wi	$$wff\left(\phi \to \psi \right)$$
6	0 2	wi	$$wff\left(\phi \to \chi \right)$$
7	5 6	wi	$$wff\left(\left(\phi \to \psi \right)\to \left(\phi \to \chi \right)\right)$$
8	4 7	wi	$$wff\left(\left(\phi \to \left(\psi \to \chi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \chi \right)\right)\right)$$