Theorem pm2.21i

A contradiction implies anything. Inference associated with pm2.21. Its associated inference is pm2.24ii. (Contributed by NM, 16-Sep-1993.)

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