Theorem mpbiran2d

Detach truth from conjunction in biconditional. Deduction form. (Contributed by Peter Mazsa, 24-Sep-2022.)

Hypotheses
mpbiran2d.1
\( \vdash \varphi \rightarrow \theta \)
mpbiran2d.2
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi) \)
Proof
l0
mpbiran2d.1
\( \vdash \varphi \rightarrow \theta \)
mpbiran2d.2
biancomd _
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \theta \wedge \chi) \)
mpbirand l0 _