bj-bi3ant

Description: This used to be in the main part. (Contributed by Wolf Lammen, 14-May-2013) (Revised by BJ, 14-Jun-2019)

		Ref	Expression
	Hypothesis	bj-bi3ant.1	$⊢ φ \to (ψ \to χ)$
	Assertion	bj-bi3ant	$⊢ ((θ \to τ) \to φ) \to (((τ \to θ) \to ψ) \to ((θ \leftrightarrow τ) \to χ))$

Step	Hyp	Ref	Expression
1		bj-bi3ant.1	$⊢ φ \to (ψ \to χ)$
2		biimp	$⊢ (θ \leftrightarrow τ) \to (θ \to τ)$
3	2	imim1i	$⊢ ((θ \to τ) \to φ) \to ((θ \leftrightarrow τ) \to φ)$
4		biimpr	$⊢ (θ \leftrightarrow τ) \to (τ \to θ)$
5	4	imim1i	$⊢ ((τ \to θ) \to ψ) \to ((θ \leftrightarrow τ) \to ψ)$
6	1	imim3i	$⊢ ((θ \leftrightarrow τ) \to φ) \to (((θ \leftrightarrow τ) \to ψ) \to ((θ \leftrightarrow τ) \to χ))$
7	3 5 6	syl2im	$⊢ ((θ \to τ) \to φ) \to (((τ \to θ) \to ψ) \to ((θ \leftrightarrow τ) \to χ))$

Metamath Proof Explorer