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; 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 379. (Contributed by NM, 30-Sep-1992.)

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  14  idALT  23  a2d  29  dfbi1ALT  204  imdi  378  sbi1  2392  difin0ss  3946  rp-fakeimass  37857