Theorem anbiim

Adding biconditional when antecedents are conjuncted. (Contributed by metakunt, 16-Apr-2024.) (Proof shortened by Wolf Lammen, 7-May-2025.) (Proof shortened by Garrett Katz, 15-Jun-2026.)

Hypotheses
anbiim.1
\( \vdash \varphi \rightarrow \chi \rightarrow \theta \)
anbiim.2
\( \vdash \psi \rightarrow \theta \rightarrow \chi \)
Conclusion
\( \vdash \varphi \wedge \psi \rightarrow (\chi \leftrightarrow \theta) \)
Proof
l0
anbiim.1
anbiim.2
impbid21d l0 _
impcom _