Theorem a1bi

Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Hypothesis
a1bi.1
\( \vdash \varphi \)
Conclusion
\( \vdash \psi \leftrightarrow \varphi \rightarrow \psi \)
Proof
l0
a1bi.1
\( \vdash \varphi \)
biimt
\( \vdash \varphi \rightarrow (\psi \leftrightarrow \varphi \rightarrow \psi) \)
ax-mp l0 _