Theorem anclb

Conjoin antecedent to left of consequent. Theorem *4.7 of [WhiteheadRussell] p. 120. (Contributed by NM, 25-Jul-1999.) (Proof shortened by Wolf Lammen, 24-Mar-2013.)

Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \varphi \wedge \psi \)
Proof
ibar
pm5.74i _