Axiom ax-frege8

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 which can be proved from only ax-mp , ax-frege1 , and ax-frege2 . (Redundant) Axiom 8 of Frege1879 p. 35. (Contributed by RP, 24-Dec-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-frege8	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜓 → ( 𝜑 → 𝜒 ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		wph	⊢ 𝜑
1		wps	⊢ 𝜓
2		wch	⊢ 𝜒
3	1 2	wi	⊢ ( 𝜓 → 𝜒 )
4	0 3	wi	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
5	0 2	wi	⊢ ( 𝜑 → 𝜒 )
6	1 5	wi	⊢ ( 𝜓 → ( 𝜑 → 𝜒 ) )
7	4 6	wi	⊢ ( ( 𝜑 → ( 𝜓 → 𝜒 ) ) → ( 𝜓 → ( 𝜑 → 𝜒 ) ) )