Axiom ax-frege8 43791

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 43772, and ax-frege2 43773. (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 36523	1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))

This axiom is referenced by:  frege26  43792  frege9  43794  frege12  43795  frege10  43802  frege17  43803  frege38  43823  frege53aid  43841  frege53a  43842  frege62a  43862  frege66a  43866  frege53b  43872  frege62b  43889  frege66b  43893  frege53c  43896  frege62c  43907  frege66c  43911  frege74  43919  frege84  43929  frege96  43941