Metamath Proof Explorer

Theorem bj-bisym

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

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

Step	Hyp	Ref	Expression
1		impbi	$⊢ (χ \to θ) \to ((θ \to χ) \to (χ \leftrightarrow θ))$
2	1	bj-bi3ant	$⊢ ((φ \to ψ) \to (χ \to θ)) \to (((ψ \to φ) \to (θ \to χ)) \to ((φ \leftrightarrow ψ) \to (χ \leftrightarrow θ)))$