Theorem pm2.61d

Deduction eliminating an antecedent. (Contributed by NM, 27-Apr-1994.) (Proof shortened by Wolf Lammen, 12-Sep-2013.)

Hypotheses
pm2.61d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
pm2.61d.2
\( \vdash \varphi \rightarrow \neg \psi \rightarrow \chi \)
Conclusion
\( \vdash \varphi \rightarrow \chi \)
Proof
pm2.61d.2
l1
con1d _
\( \vdash \varphi \rightarrow \neg \chi \rightarrow \psi \)
pm2.61d.1
\( \vdash \varphi \rightarrow \psi \rightarrow \chi \)
syld l1 _
pm2.18d _