Axiom ax-2 7

Description: Axiom Frege. 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 as Frege in the literature. 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 353. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
ax-2	|- ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))

Detailed syntax breakdown of Axiom ax-2

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2		wps	. . . 4 wff ps
3		wch	. . . 4 wff ch
4	2, 3	wi 4	. . 3 wff (ps -> ch)
5	1, 4	wi 4	. 2 wff (ph -> (ps -> ch))
6	1, 2	wi 4	. . 3 wff (ph -> ps)
7	1, 3	wi 4	. . 3 wff (ph -> ch)
8	6, 7	wi 4	. 2 wff ((ph -> ps) -> (ph -> ch))
9	5, 8	wi 4	1 wff ((ph -> (ps -> ch)) -> ((ph -> ps) -> (ph -> ch)))

This axiom is referenced by:  a2i  12  idALT  20  a2d  23  dfbi1gb  185  imdi  352  sbi1  2063  ralim  2686  difin0ss  3617