Theorem ccase2

Inference for combining cases. (Contributed by NM, 29-Jul-1999.)

Hypotheses
ccase2.1
\( \vdash \varphi \wedge \psi \rightarrow \tau \)
ccase2.2
\( \vdash \chi \rightarrow \tau \)
ccase2.3
\( \vdash \theta \rightarrow \tau \)
Conclusion
\( \vdash (\varphi \vee \chi) \wedge (\psi \vee \theta) \rightarrow \tau \)
Proof
l0
ccase2.1
ccase2.2
l2
adantr _
ccase2.3
l4
adantl _
ccase2.3
adantl _
ccase l0 l2 l4 _