Theorem anbiimOLD

Obsolete version of anbiim as of 15-Jun-2026. Adding biconditional when antecedents are conjuncted. (Contributed by metakunt, 16-Apr-2024.) (Proof shortened by Wolf Lammen, 7-May-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

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
anbiim.1
l1
adantr _
anbiim.2
adantl _
impbid l1 _