Theorem pm4.71rd

Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by NM, 10-Feb-2005.)

Hypothesis
pm4.71rd.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \psi) \)
Proof
pm4.71rd.1
pm4.71d _
biancomd _