Theorem
ibar
Introduction of antecedent as conjunct. (Contributed by NM, 5-Dec-1995.)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \varphi \wedge \psi) \)
Proof
iba
biancomd
_
This is the content in the right pane.