Axiom ax-frege8 44612

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 44593, and ax-frege2 44594. (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 37192	1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))

This axiom is used by:  frege26  44613  frege9  44615  frege12  44616  frege10  44623  frege17  44624  frege38  44644  frege53aid  44662  frege53a  44663  frege62a  44683  frege66a  44687  frege53b  44693  frege62b  44710  frege66b  44714  frege53c  44717  frege62c  44728  frege66c  44732  frege74  44740  frege84  44750  frege96  44762