Axiom ax-frege8 40148

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 40129, and ax-frege2 40130. (Redundant) Axiom 8 of [Frege1879] p. 35. (Contributed by RP, 24-Dec-2019.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-frege8	⊢ ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))

Detailed syntax breakdown of Axiom ax-frege8

Step	Hyp	Ref	Expression
1		wph	. 2 wff 𝜑
2		wps	. . 3 wff 𝜓
3		wch	. . 3 wff 𝜒
4	2, 3	wi 4	. 2 wff (𝜓 → 𝜒)
5	1, 3	wi 4	. . 3 wff (𝜑 → 𝜒)
6	2, 5	wi 4	. 2 wff (𝜓 → (𝜑 → 𝜒))
7	1, 4, 6	bj-0 33876	1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))

This axiom is referenced by:  frege26  40149  frege9  40151  frege12  40152  frege10  40159  frege17  40160  frege38  40180  frege53aid  40198  frege53a  40199  frege62a  40219  frege66a  40223  frege53b  40229  frege62b  40246  frege66b  40250  frege53c  40253  frege62c  40264  frege66c  40268  frege74  40276  frege84  40286  frege96  40298