Axiom ax-2 7

Description: Axiom Frege. Axiom A2 of [Margaris] p. 49. This axiom "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 250. (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  11  idALT  20  a2d  26  imdi  249  sbi1v  1879  ralim  2524