Theorem a1i

Inference introducing an antecedent. Inference associated with [ax-1]. Its associated inference is a1ii. See [conventions] for a definition of "associated inference". (Contributed by NM, 29-Dec-1992.)

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