Metamath Proof Explorer


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 θτφτθψθτχ