Theorem mpbirand

Detach truth from conjunction in biconditional. (Contributed by Glauco Siliprandi, 3-Mar-2021.)

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