# Metamath Proof Explorer

## Theorem 3jaodan

Description: Disjunction of three antecedents (deduction). (Contributed by NM, 14-Oct-2005)

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

### Proof

Step Hyp Ref Expression
1 3jaodan.1 ${⊢}\left({\phi }\wedge {\psi }\right)\to {\chi }$
2 3jaodan.2 ${⊢}\left({\phi }\wedge {\theta }\right)\to {\chi }$
3 3jaodan.3 ${⊢}\left({\phi }\wedge {\tau }\right)\to {\chi }$
4 1 ex ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
5 2 ex ${⊢}{\phi }\to \left({\theta }\to {\chi }\right)$
6 3 ex ${⊢}{\phi }\to \left({\tau }\to {\chi }\right)$
7 4 5 6 3jaod ${⊢}{\phi }\to \left(\left({\psi }\vee {\theta }\vee {\tau }\right)\to {\chi }\right)$
8 7 imp ${⊢}\left({\phi }\wedge \left({\psi }\vee {\theta }\vee {\tau }\right)\right)\to {\chi }$