Theorem 4cases

Inference eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 25-Oct-2003.)

Hypotheses
4cases.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
4cases.2
\( \vdash \varphi \wedge \neg \psi \rightarrow \chi \)
4cases.3
\( \vdash \neg \varphi \wedge \psi \rightarrow \chi \)
4cases.4
\( \vdash \neg \varphi \wedge \neg \psi \rightarrow \chi \)
Conclusion
\( \vdash \chi \)
Proof
l0
4cases.1
\( \vdash \varphi \wedge \psi \rightarrow \chi \)
4cases.3
\( \vdash \neg \varphi \wedge \psi \rightarrow \chi \)
l2
pm2.61ian l0 _
\( \vdash \psi \rightarrow \chi \)
l3
4cases.2
\( \vdash \varphi \wedge \neg \psi \rightarrow \chi \)
4cases.4
\( \vdash \neg \varphi \wedge \neg \psi \rightarrow \chi \)
pm2.61ian l3 _
\( \vdash \neg \psi \rightarrow \chi \)
pm2.61i l2 _