Axiom ax-frege8 37123

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 88 which can be proved from only ax-mp 5, ax-frege1 37104, and ax-frege2 37105. (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 31703	1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))

This axiom is referenced by:  frege26  37124  frege9  37126  frege12  37127  frege10  37134  frege17  37135  frege38  37155  frege53aid  37173  frege53a  37174  frege62a  37194  frege66a  37198  frege53b  37204  frege62b  37221  frege66b  37225  frege53c  37228  frege62c  37239  frege66c  37243  frege74  37251  frege84  37261  frege96  37273