# Metamath Proof Explorer

## Theorem ccased

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

Ref Expression
Hypotheses ccased.1 ${⊢}{\phi }\to \left(\left({\psi }\wedge {\chi }\right)\to {\eta }\right)$
ccased.2 ${⊢}{\phi }\to \left(\left({\theta }\wedge {\chi }\right)\to {\eta }\right)$
ccased.3 ${⊢}{\phi }\to \left(\left({\psi }\wedge {\tau }\right)\to {\eta }\right)$
ccased.4 ${⊢}{\phi }\to \left(\left({\theta }\wedge {\tau }\right)\to {\eta }\right)$
Assertion ccased ${⊢}{\phi }\to \left(\left(\left({\psi }\vee {\theta }\right)\wedge \left({\chi }\vee {\tau }\right)\right)\to {\eta }\right)$

### Proof

Step Hyp Ref Expression
1 ccased.1 ${⊢}{\phi }\to \left(\left({\psi }\wedge {\chi }\right)\to {\eta }\right)$
2 ccased.2 ${⊢}{\phi }\to \left(\left({\theta }\wedge {\chi }\right)\to {\eta }\right)$
3 ccased.3 ${⊢}{\phi }\to \left(\left({\psi }\wedge {\tau }\right)\to {\eta }\right)$
4 ccased.4 ${⊢}{\phi }\to \left(\left({\theta }\wedge {\tau }\right)\to {\eta }\right)$
5 1 com12 ${⊢}\left({\psi }\wedge {\chi }\right)\to \left({\phi }\to {\eta }\right)$
6 2 com12 ${⊢}\left({\theta }\wedge {\chi }\right)\to \left({\phi }\to {\eta }\right)$
7 3 com12 ${⊢}\left({\psi }\wedge {\tau }\right)\to \left({\phi }\to {\eta }\right)$
8 4 com12 ${⊢}\left({\theta }\wedge {\tau }\right)\to \left({\phi }\to {\eta }\right)$
9 5 6 7 8 ccase ${⊢}\left(\left({\psi }\vee {\theta }\right)\wedge \left({\chi }\vee {\tau }\right)\right)\to \left({\phi }\to {\eta }\right)$
10 9 com12 ${⊢}{\phi }\to \left(\left(\left({\psi }\vee {\theta }\right)\wedge \left({\chi }\vee {\tau }\right)\right)\to {\eta }\right)$