Metamath Proof Explorer

Theorem frege10

Description: Result commuting antecedents within an antecedent. Proposition 10 of Frege1879 p. 36. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

		Ref	Expression
	Assertion	frege10	$⊢ ((φ \to (ψ \to χ)) \to θ) \to ((ψ \to (φ \to χ)) \to θ)$

Proof

Step	Hyp	Ref	Expression
1		ax-frege8	$⊢ (ψ \to (φ \to χ)) \to (φ \to (ψ \to χ))$
2		frege9	$⊢ ((ψ \to (φ \to χ)) \to (φ \to (ψ \to χ))) \to (((φ \to (ψ \to χ)) \to θ) \to ((ψ \to (φ \to χ)) \to θ))$
3	1 2	ax-mp	$⊢ ((φ \to (ψ \to χ)) \to θ) \to ((ψ \to (φ \to χ)) \to θ)$