# Metamath Proof Explorer

## Theorem syl133anc

Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012)

Ref Expression
Hypotheses syl3anc.1 ${⊢}{\phi }\to {\psi }$
syl3anc.2 ${⊢}{\phi }\to {\chi }$
syl3anc.3 ${⊢}{\phi }\to {\theta }$
syl3Xanc.4 ${⊢}{\phi }\to {\tau }$
syl23anc.5 ${⊢}{\phi }\to {\eta }$
syl33anc.6 ${⊢}{\phi }\to {\zeta }$
syl133anc.7 ${⊢}{\phi }\to {\sigma }$
syl133anc.8 ${⊢}\left({\psi }\wedge \left({\chi }\wedge {\theta }\wedge {\tau }\right)\wedge \left({\eta }\wedge {\zeta }\wedge {\sigma }\right)\right)\to {\rho }$
Assertion syl133anc ${⊢}{\phi }\to {\rho }$

### Proof

Step Hyp Ref Expression
1 syl3anc.1 ${⊢}{\phi }\to {\psi }$
2 syl3anc.2 ${⊢}{\phi }\to {\chi }$
3 syl3anc.3 ${⊢}{\phi }\to {\theta }$
4 syl3Xanc.4 ${⊢}{\phi }\to {\tau }$
5 syl23anc.5 ${⊢}{\phi }\to {\eta }$
6 syl33anc.6 ${⊢}{\phi }\to {\zeta }$
7 syl133anc.7 ${⊢}{\phi }\to {\sigma }$
8 syl133anc.8 ${⊢}\left({\psi }\wedge \left({\chi }\wedge {\theta }\wedge {\tau }\right)\wedge \left({\eta }\wedge {\zeta }\wedge {\sigma }\right)\right)\to {\rho }$
9 5 6 7 3jca ${⊢}{\phi }\to \left({\eta }\wedge {\zeta }\wedge {\sigma }\right)$
10 1 2 3 4 9 8 syl131anc ${⊢}{\phi }\to {\rho }$