Axiom ax-frege8 44652

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 91 which can be proved from only ax-mp 5, ax-frege1 44633, and ax-frege2 44634. (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 37242	1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))

This axiom is used by:  frege26  44653  frege9  44655  frege12  44656  frege10  44663  frege17  44664  frege38  44684  frege53aid  44702  frege53a  44703  frege62a  44723  frege66a  44727  frege53b  44733  frege62b  44750  frege66b  44754  frege53c  44757  frege62c  44768  frege66c  44772  frege74  44780  frege84  44790  frege96  44802