Theorem pm2.24i

Inference associated with pm2.24. Its associated inference is pm2.24ii. (Contributed by NM, 20-Aug-2001.)

Hypothesis
pm2.24i.1
\( \vdash \varphi \)
Conclusion
\( \vdash \neg \varphi \rightarrow \psi \)
Proof
pm2.24i.1
a1i _
con1i _