Metamath Proof Explorer

Theorem bj-imim11

Description: The propositional function ( ( . -> ph ) -> ps ) is increasing. (Contributed by BJ, 3-Apr-2026)

		Ref	Expression
	Assertion	bj-imim11	$⊢ (φ \to ψ) \to (((φ \to χ) \to θ) \to ((ψ \to χ) \to θ))$

Step	Hyp	Ref	Expression
1		imim1	$⊢ (φ \to ψ) \to ((ψ \to χ) \to (φ \to χ))$
2	1	imim1d	$⊢ (φ \to ψ) \to (((φ \to χ) \to θ) \to ((ψ \to χ) \to θ))$