Theorem bi23imp13

3imp with middle implication of the hypothesis a biconditional. (Contributed by Alan Sare, 6-Nov-2017.)

Hypothesis
bi23imp13.1
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \rightarrow \theta) \)
Conclusion
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
Proof
bi23imp13.1
biimpd _
3imp _