Theorem biadanid

Deduction associated with biadani. Add a conjunction to an equivalence. (Contributed by Thierry Arnoux, 16-Jun-2024.)

Hypotheses
biadanid.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
biadanid.2
\( \vdash \varphi \wedge \chi \rightarrow (\psi \leftrightarrow \theta) \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \chi \wedge \theta) \)
Proof
l0
biadanid.1
l1
biadanid.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
biadanid.2
biimpa _
an32s _
\( \vdash \varphi \wedge \psi \wedge \chi \rightarrow \theta \)
mpdan l1 _
l6
jca l0 _
biadanid.2
biimpar _
anasss _
impbida l6 _