# Metamath Proof Explorer

## Theorem syl223anc

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