Theorem pm2.18d

Deduction form of the Clavius law pm2.18. (Contributed by FL, 12-Jul-2009.) (Proof shortened by Andrew Salmon, 7-May-2011.) Shorten pm2.18. (Revised by Wolf Lammen, 17-Nov-2023.)

Hypothesis
pm2.18d.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \psi \)
Conclusion
\( \vdash \varphi \rightarrow \psi \)
Proof
l0
id
\( \vdash \varphi \rightarrow \varphi \)
l1
pm2.18d.1
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \psi \)
pm2.21
\( \vdash \neg \psi \rightarrow \psi \rightarrow \neg \varphi \)
sylcom l1 _
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \neg \varphi \)
mt4d l0 _