Theorem pm2.61iii

Inference eliminating three antecedents. (Contributed by NM, 2-Jan-2002.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypotheses
pm2.61iii.1
\( \vdash \neg \varphi \rightarrow \neg \psi \rightarrow \neg \chi \rightarrow \theta \)
pm2.61iii.2
\( \vdash \varphi \rightarrow \theta \)
pm2.61iii.3
\( \vdash \psi \rightarrow \theta \)
pm2.61iii.4
\( \vdash \chi \rightarrow \theta \)
Conclusion
\( \vdash \theta \)
Proof
l0
pm2.61iii.4
\( \vdash \chi \rightarrow \theta \)
l1
pm2.61iii.1
\( \vdash \neg \varphi \rightarrow \neg \psi \rightarrow \neg \chi \rightarrow \theta \)
pm2.61iii.2
l3
a1d _
\( \vdash \varphi \rightarrow \neg \chi \rightarrow \theta \)
pm2.61iii.3
a1d _
\( \vdash \psi \rightarrow \neg \chi \rightarrow \theta \)
pm2.61ii l1 l3 _
\( \vdash \neg \chi \rightarrow \theta \)
pm2.61i l0 _