Theorem pm4.71d

Deduction converting an implication to a biconditional with conjunction. Deduction from Theorem *4.71 of [WhiteheadRussell] p. 120. (Contributed by Mario Carneiro, 25-Dec-2016.)

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