Theorem pm4.71

Implication in terms of biconditional and conjunction. Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 2-Dec-2012.)

Conclusion
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\varphi \leftrightarrow \varphi \wedge \psi) \)
Proof
simpl
l1
biantru _
\( \vdash \varphi \rightarrow \varphi \wedge \psi \leftrightarrow (\varphi \rightarrow \varphi \wedge \psi) \wedge (\varphi \wedge \psi \rightarrow \varphi) \)
l2
anclb
\( \vdash \varphi \rightarrow \psi \leftrightarrow \varphi \rightarrow \varphi \wedge \psi \)
dfbi2
\( \vdash \varphi \leftrightarrow \varphi \wedge \psi \leftrightarrow (\varphi \rightarrow \varphi \wedge \psi) \wedge (\varphi \wedge \psi \rightarrow \varphi) \)
3bitr4i l1 l2 _