Theorem syl332anc 1357

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

Hypotheses

Ref	Expression
syl12anc.1	|- ( ph -> ps )
syl12anc.2	|- ( ph -> ch )
syl12anc.3	|- ( ph -> th )
syl22anc.4	|- ( ph -> ta )
syl23anc.5	|- ( ph -> et )
syl33anc.6	|- ( ph -> ze )
syl133anc.7	|- ( ph -> si )
syl233anc.8	|- ( ph -> rh )
syl332anc.9	|- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et /\ ze ) /\ ( si /\ rh ) ) -> mu )

Assertion

Ref	Expression
syl332anc	|- ( ph -> mu )

Proof of Theorem syl332anc

Step	Hyp	Ref	Expression
1		syl12anc.1	. 2 |- ( ph -> ps )
2		syl12anc.2	. 2 |- ( ph -> ch )
3		syl12anc.3	. 2 |- ( ph -> th )
4		syl22anc.4	. 2 |- ( ph -> ta )
5		syl23anc.5	. 2 |- ( ph -> et )
6		syl33anc.6	. 2 |- ( ph -> ze )
7		syl133anc.7	. . 3 |- ( ph -> si )
8		syl233anc.8	. . 3 |- ( ph -> rh )
9	7, 8	jca 554	. 2 |- ( ph -> ( si /\ rh ) )
10		syl332anc.9	. 2 |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et /\ ze ) /\ ( si /\ rh ) ) -> mu )
11	1, 2, 3, 4, 5, 6, 9, 10	syl331anc 1351	1 |- ( ph -> mu )

Syntax hints:   -> wi 4   /\ wa 384   /\ w3a 1037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197  df-an 386  df-3an 1039

This theorem is referenced by:  mdetunilem5  20422  mdetuni0  20427  lnjatN  35066  lncmp  35069  cdlema1N  35077  4atexlemex6  35360  cdlemd4  35488  cdleme18c  35580  cdleme18d  35582  cdleme19b  35592  cdleme21ct  35617  cdleme21d  35618  cdleme21e  35619  cdleme21k  35626  cdleme22g  35636  cdleme24  35640  cdleme27a  35655  cdleme27N  35657  cdleme28a  35658  cdleme40n  35756  cdlemg16zz  35948  cdlemg37  35977  cdlemk21-2N  36179  cdlemk20-2N  36180  cdlemk28-3  36196  cdlemk19xlem  36230