Theorem pm2.24ii

A contradiction implies anything. Inference associated with pm2.21i and pm2.24i. (Contributed by NM, 27-Feb-2008.)

Hypotheses
pm2.24ii.1
\( \vdash \varphi \)
pm2.24ii.2
\( \vdash \neg \varphi \)
Conclusion
\( \vdash \psi \)
Proof
l0
pm2.24ii.1
\( \vdash \varphi \)
pm2.24ii.2
pm2.21i _
\( \vdash \varphi \rightarrow \psi \)
ax-mp l0 _