Theorem ccased

Deduction for combining cases. (Contributed by NM, 9-May-2004.)

Hypotheses
ccased.1
\( \vdash \varphi \rightarrow \psi \wedge \chi \rightarrow \eta \)
ccased.2
\( \vdash \varphi \rightarrow \theta \wedge \chi \rightarrow \eta \)
ccased.3
\( \vdash \varphi \rightarrow \psi \wedge \tau \rightarrow \eta \)
ccased.4
\( \vdash \varphi \rightarrow \theta \wedge \tau \rightarrow \eta \)
Conclusion
\( \vdash \varphi \rightarrow (\psi \vee \theta) \wedge (\chi \vee \tau) \rightarrow \eta \)
Proof
ccased.1
l1
com12 _
ccased.2
l3
com12 _
ccased.3
l5
com12 _
ccased.4
com12 _
ccase l1 l3 l5 _
com12 _