Theorem bilani

Inference adding a conjunct to the left-hand side of a biconditional. (Contributed by Matthew House, 22-May-2026.)

Hypothesis
birani.1
\( \vdash \varphi \leftrightarrow \psi \)
Conclusion
\( \vdash \chi \wedge \varphi \rightarrow \psi \)
Proof
birani.1
biimpi _
adantl _