# Metamath Proof Explorer

## Theorem ecase23d

Description: Deduction for elimination by cases. (Contributed by NM, 22-Apr-1994)

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

### Proof

Step Hyp Ref Expression
1 ecase23d.1 ${⊢}{\phi }\to ¬{\chi }$
2 ecase23d.2 ${⊢}{\phi }\to ¬{\theta }$
3 ecase23d.3 ${⊢}{\phi }\to \left({\psi }\vee {\chi }\vee {\theta }\right)$
4 ioran ${⊢}¬\left({\chi }\vee {\theta }\right)↔\left(¬{\chi }\wedge ¬{\theta }\right)$
5 1 2 4 sylanbrc ${⊢}{\phi }\to ¬\left({\chi }\vee {\theta }\right)$
6 3orass ${⊢}\left({\psi }\vee {\chi }\vee {\theta }\right)↔\left({\psi }\vee \left({\chi }\vee {\theta }\right)\right)$
7 3 6 sylib ${⊢}{\phi }\to \left({\psi }\vee \left({\chi }\vee {\theta }\right)\right)$
8 7 ord ${⊢}{\phi }\to \left(¬{\psi }\to \left({\chi }\vee {\theta }\right)\right)$
9 5 8 mt3d ${⊢}{\phi }\to {\psi }$