Metamath Proof Explorer

Theorem frege4

Description: Special case of closed form of a2d . Special case of rp-frege4g . Proposition 4 of Frege1879 p. 31. (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		frege3	$⊢ (φ \to ψ) \to ((χ \to (φ \to ψ)) \to ((χ \to φ) \to (χ \to ψ)))$
2		ax-frege2	$⊢ ((φ \to ψ) \to ((χ \to (φ \to ψ)) \to ((χ \to φ) \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 ((χ \to φ) \to (χ \to ψ)))$