Theorem biranri

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