Axiom ax-frege8 44461

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 44442, and ax-frege2 44443. (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 37054	1 wff ((𝜑 → (𝜓 → 𝜒)) → (𝜓 → (𝜑 → 𝜒)))

This axiom is referenced by:  frege26  44462  frege9  44464  frege12  44465  frege10  44472  frege17  44473  frege38  44493  frege53aid  44511  frege53a  44512  frege62a  44532  frege66a  44536  frege53b  44542  frege62b  44559  frege66b  44563  frege53c  44566  frege62c  44577  frege66c  44581  frege74  44589  frege84  44599  frege96  44611