Theorem pm2.61i

Inference eliminating an antecedent. (Contributed by NM, 5-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2023.)

Hypotheses
pm2.61i.1
\( \vdash \varphi \rightarrow \psi \)
pm2.61i.2
\( \vdash \neg \varphi \rightarrow \psi \)
Conclusion
\( \vdash \psi \)
Proof
l0
pm2.61i.1
\( \vdash \varphi \rightarrow \psi \)
pm2.61i.2
\( \vdash \neg \varphi \rightarrow \psi \)
nsyl4 l0 _
pm2.18i _