Theorem bija

Combine antecedents into a single biconditional. This inference, reminiscent of ja, is reversible: The hypotheses can be deduced from the conclusion alone (see pm5.1im and pm5.21im ). (Contributed by Wolf Lammen, 13-May-2013.)

Hypotheses
bija.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
bija.2
\( \vdash \neg \varphi \rightarrow \neg \psi \rightarrow \chi \)
Conclusion
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow \chi \)
Proof
l0
biimpr
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow \psi \rightarrow \varphi \)
bija.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
l2
syli l0 _
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow \psi \rightarrow \chi \)
biimp
l4
con3d _
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow \neg \psi \rightarrow \neg \varphi \)
bija.2
\( \vdash \neg \varphi \rightarrow \neg \psi \rightarrow \chi \)
syli l4 _
\( \vdash (\varphi \leftrightarrow \psi) \rightarrow \neg \psi \rightarrow \chi \)
pm2.61d l2 _