Theorem pm4.71r

Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 25-Jul-1999.)

Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\varphi \leftrightarrow \psi \wedge \varphi) \)
Proof
l0
pm4.71
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\varphi \leftrightarrow \varphi \wedge \psi) \)
ancom
bibi2i _
\( \vdash \varphi \leftrightarrow \varphi \wedge \psi \leftrightarrow (\varphi \leftrightarrow \psi \wedge \varphi) \)
bitri l0 _