Theorem ccase

Inference for combining cases. (Contributed by NM, 29-Jul-1999.) (Proof shortened by Wolf Lammen, 6-Jan-2013.)

Hypotheses
ccase.1
\( \vdash \varphi \wedge \psi \rightarrow \tau \)
ccase.2
\( \vdash \chi \wedge \psi \rightarrow \tau \)
ccase.3
\( \vdash \varphi \wedge \theta \rightarrow \tau \)
ccase.4
\( \vdash \chi \wedge \theta \rightarrow \tau \)
Conclusion
\( \vdash (\varphi \vee \chi) \wedge (\psi \vee \theta) \rightarrow \tau \)
Proof
l0
ccase.1
ccase.2
l2
jaoian l0 _
l3
ccase.3
ccase.4
jaoian l3 _
jaodan l2 _