# Metamath Proof Explorer

## Theorem 3jaao

Description: Inference conjoining and disjoining the antecedents of three implications. (Contributed by Jeff Hankins, 15-Aug-2009) (Proof shortened by Andrew Salmon, 13-May-2011)

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

### Proof

Step Hyp Ref Expression
1 3jaao.1 ${⊢}{\phi }\to \left({\psi }\to {\chi }\right)$
2 3jaao.2 ${⊢}{\theta }\to \left({\tau }\to {\chi }\right)$
3 3jaao.3 ${⊢}{\eta }\to \left({\zeta }\to {\chi }\right)$
4 1 3ad2ant1 ${⊢}\left({\phi }\wedge {\theta }\wedge {\eta }\right)\to \left({\psi }\to {\chi }\right)$
5 2 3ad2ant2 ${⊢}\left({\phi }\wedge {\theta }\wedge {\eta }\right)\to \left({\tau }\to {\chi }\right)$
6 3 3ad2ant3 ${⊢}\left({\phi }\wedge {\theta }\wedge {\eta }\right)\to \left({\zeta }\to {\chi }\right)$
7 4 5 6 3jaod ${⊢}\left({\phi }\wedge {\theta }\wedge {\eta }\right)\to \left(\left({\psi }\vee {\tau }\vee {\zeta }\right)\to {\chi }\right)$