Theorem birani

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 \varphi \wedge \chi \rightarrow \psi \)
Proof
birani.1
biimpi _
adantr _