Axiom ax-frege8 38103

Description: Swap antecedents. If two conditions have a proposition as a consequence, their order is immaterial. Third axiom of Frege's 1879 work but identical to pm2.04 90 which can be proved from only ax-mp 5, ax-frege1 38084, and ax-frege2 38085. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)

Assertion

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

Detailed syntax breakdown of Axiom ax-frege8

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

This axiom is referenced by:  frege26  38104  frege9  38106  frege12  38107  frege10  38114  frege17  38115  frege38  38135  frege53aid  38153  frege53a  38154  frege62a  38174  frege66a  38178  frege53b  38184  frege62b  38201  frege66b  38205  frege53c  38208  frege62c  38219  frege66c  38223  frege74  38231  frege84  38241  frege96  38253