# Metamath Proof Explorer

## Theorem syl132anc

Description: Syllogism combined with contraction. (Contributed by NM, 11-Jul-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 }$
syl132anc.7 ${⊢}\left({\psi }\wedge \left({\chi }\wedge {\theta }\wedge {\tau }\right)\wedge \left({\eta }\wedge {\zeta }\right)\right)\to {\sigma }$
Assertion syl132anc ${⊢}{\phi }\to {\sigma }$

### 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 syl132anc.7 ${⊢}\left({\psi }\wedge \left({\chi }\wedge {\theta }\wedge {\tau }\right)\wedge \left({\eta }\wedge {\zeta }\right)\right)\to {\sigma }$
8 5 6 jca ${⊢}{\phi }\to \left({\eta }\wedge {\zeta }\right)$
9 1 2 3 4 8 7 syl131anc ${⊢}{\phi }\to {\sigma }$