Theorem abai

Introduce one conjunct as an antecedent to the other. "abai" stands for "and, biconditional, and, implication". (Contributed by NM, 12-Aug-1993.) (Proof shortened by Wolf Lammen, 7-Dec-2012.)

Conclusion
\( \vdash \varphi \wedge \psi \leftrightarrow \varphi \wedge (\varphi \rightarrow \psi) \)
Proof
biimt
pm5.32i _