Theorem
biimpac
Importation inference from a logical equivalence. (Contributed by NM, 3-May-1994.)
Hypothesis
biimpa.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Conclusion
\( \vdash \psi \wedge \varphi \rightarrow \chi \)
Proof
biimpa.1
biimpcd
_
imp
_
This is the content in the right pane.