Theorem biadanii

Inference associated with biadani. Add a conjunction to an equivalence. (Contributed by Jeff Madsen, 20-Jun-2011.) (Proof shortened by BJ, 4-Mar-2023.)

Hypotheses
biadani.1
\( \vdash \varphi \rightarrow \psi \)
biadanii.2
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi) \)
Conclusion
\( \vdash \varphi \leftrightarrow \psi \wedge \chi \)
Proof
l0
biadanii.2
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi) \)
biadani.1
biadani _
\( \vdash \psi \rightarrow (\varphi \leftrightarrow \chi) \leftrightarrow (\varphi \leftrightarrow \psi \wedge \chi) \)
mpbi l0 _