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	|- ( ph -> ( ps -> ch ) )
Assertion	bj-bi3ant	|- ( ( ( th -> ta ) -> ph ) -> ( ( ( ta -> th ) -> ps ) -> ( ( th <-> ta ) -> ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		bj-bi3ant.1	|- ( ph -> ( ps -> ch ) )
2		biimp	|- ( ( th <-> ta ) -> ( th -> ta ) )
3	2	imim1i	|- ( ( ( th -> ta ) -> ph ) -> ( ( th <-> ta ) -> ph ) )
4		biimpr	|- ( ( th <-> ta ) -> ( ta -> th ) )
5	4	imim1i	|- ( ( ( ta -> th ) -> ps ) -> ( ( th <-> ta ) -> ps ) )
6	1	imim3i	|- ( ( ( th <-> ta ) -> ph ) -> ( ( ( th <-> ta ) -> ps ) -> ( ( th <-> ta ) -> ch ) ) )
7	3 5 6	syl2im	|- ( ( ( th -> ta ) -> ph ) -> ( ( ( ta -> th ) -> ps ) -> ( ( th <-> ta ) -> ch ) ) )