# Metamath Proof Explorer

## Theorem syl231anc

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