Theorem 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	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
Assertion	bj-bi3ant	⊢ ( ( ( 𝜃 → 𝜏 ) → 𝜑 ) → ( ( ( 𝜏 → 𝜃 ) → 𝜓 ) → ( ( 𝜃 ↔ 𝜏 ) → 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-bi3ant.1	⊢ ( 𝜑 → ( 𝜓 → 𝜒 ) )
2		biimp	⊢ ( ( 𝜃 ↔ 𝜏 ) → ( 𝜃 → 𝜏 ) )
3	2	imim1i	⊢ ( ( ( 𝜃 → 𝜏 ) → 𝜑 ) → ( ( 𝜃 ↔ 𝜏 ) → 𝜑 ) )
4		biimpr	⊢ ( ( 𝜃 ↔ 𝜏 ) → ( 𝜏 → 𝜃 ) )
5	4	imim1i	⊢ ( ( ( 𝜏 → 𝜃 ) → 𝜓 ) → ( ( 𝜃 ↔ 𝜏 ) → 𝜓 ) )
6	1	imim3i	⊢ ( ( ( 𝜃 ↔ 𝜏 ) → 𝜑 ) → ( ( ( 𝜃 ↔ 𝜏 ) → 𝜓 ) → ( ( 𝜃 ↔ 𝜏 ) → 𝜒 ) ) )
7	3 5 6	syl2im	⊢ ( ( ( 𝜃 → 𝜏 ) → 𝜑 ) → ( ( ( 𝜏 → 𝜃 ) → 𝜓 ) → ( ( 𝜃 ↔ 𝜏 ) → 𝜒 ) ) )