Theorem 4casesdan

Deduction eliminating two antecedents from the four possible cases that result from their true/false combinations. (Contributed by NM, 19-Mar-2013.)

Hypotheses
4casesdan.1
\( \vdash \varphi \wedge (\psi \wedge \chi) \rightarrow \theta \)
4casesdan.2
\( \vdash \varphi \wedge (\psi \wedge \neg \chi) \rightarrow \theta \)
4casesdan.3
\( \vdash \varphi \wedge (\neg \psi \wedge \chi) \rightarrow \theta \)
4casesdan.4
\( \vdash \varphi \wedge (\neg \psi \wedge \neg \chi) \rightarrow \theta \)
Conclusion
\( \vdash \varphi \rightarrow \theta \)
Proof
4casesdan.1
l1
expcom _
\( \vdash \psi \wedge \chi \rightarrow \varphi \rightarrow \theta \)
4casesdan.2
l3
expcom _
\( \vdash \psi \wedge \neg \chi \rightarrow \varphi \rightarrow \theta \)
4casesdan.3
l5
expcom _
\( \vdash \neg \psi \wedge \chi \rightarrow \varphi \rightarrow \theta \)
4casesdan.4
expcom _
\( \vdash \neg \psi \wedge \neg \chi \rightarrow \varphi \rightarrow \theta \)
4cases l1 l3 l5 _