Theorem pm4.71i

Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 4-Jan-2004.)

Hypothesis
pm4.71i.1
\( \vdash \varphi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \leftrightarrow \varphi \wedge \psi \)
Proof
l0
pm4.71i.1
\( \vdash \varphi \rightarrow \psi \)
pm4.71
\( \vdash \varphi \rightarrow \psi \leftrightarrow (\varphi \leftrightarrow \varphi \wedge \psi) \)
mpbi l0 _