Metamath Proof Explorer

Theorem rp-6frege

Description: Elimination of a nested antecedent of special form. (Contributed by RP, 24-Dec-2019)

		Ref	Expression
	Assertion	rp-6frege	$⊢ φ \to ((ψ \to ((χ \to ψ) \to θ)) \to (ψ \to θ))$

Step	Hyp	Ref	Expression
1		rp-4frege	$⊢ (ψ \to ((χ \to ψ) \to θ)) \to (ψ \to θ)$
2		ax-frege1	$⊢ ((ψ \to ((χ \to ψ) \to θ)) \to (ψ \to θ)) \to (φ \to ((ψ \to ((χ \to ψ) \to θ)) \to (ψ \to θ)))$
3	1 2	ax-mp	$⊢ φ \to ((ψ \to ((χ \to ψ) \to θ)) \to (ψ \to θ))$