# Metamath Proof Explorer

## Theorem 4casesdan

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

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

### Proof

Step Hyp Ref Expression
1 4casesdan.1 ${⊢}\left({\phi }\wedge \left({\psi }\wedge {\chi }\right)\right)\to {\theta }$
2 4casesdan.2 ${⊢}\left({\phi }\wedge \left({\psi }\wedge ¬{\chi }\right)\right)\to {\theta }$
3 4casesdan.3 ${⊢}\left({\phi }\wedge \left(¬{\psi }\wedge {\chi }\right)\right)\to {\theta }$
4 4casesdan.4 ${⊢}\left({\phi }\wedge \left(¬{\psi }\wedge ¬{\chi }\right)\right)\to {\theta }$
5 1 expcom ${⊢}\left({\psi }\wedge {\chi }\right)\to \left({\phi }\to {\theta }\right)$
6 2 expcom ${⊢}\left({\psi }\wedge ¬{\chi }\right)\to \left({\phi }\to {\theta }\right)$
7 3 expcom ${⊢}\left(¬{\psi }\wedge {\chi }\right)\to \left({\phi }\to {\theta }\right)$
8 4 expcom ${⊢}\left(¬{\psi }\wedge ¬{\chi }\right)\to \left({\phi }\to {\theta }\right)$
9 5 6 7 8 4cases ${⊢}{\phi }\to {\theta }$