Theorem bilanri

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

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