Theorem pm4.71ri

Inference converting an implication to a biconditional with conjunction. Inference from Theorem *4.71 of [WhiteheadRussell] p. 120 (with conjunct reversed). (Contributed by NM, 1-Dec-2003.)

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