Theorem syl333anc 1358

Description: A syllogism inference combined with contraction. (Contributed by NM, 10-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 )
syl333anc.9	|- ( ph -> mu )
syl333anc.10	|- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et /\ ze ) /\ ( si /\ rh /\ mu ) ) -> la )

Assertion

Ref	Expression
syl333anc	|- ( ph -> la )

Proof of Theorem syl333anc

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		syl333anc.9	. . 3 |- ( ph -> mu )
10	7, 8, 9	3jca 1242	. 2 |- ( ph -> ( si /\ rh /\ mu ) )
11		syl333anc.10	. 2 |- ( ( ( ps /\ ch /\ th ) /\ ( ta /\ et /\ ze ) /\ ( si /\ rh /\ mu ) ) -> la )
12	1, 2, 3, 4, 5, 6, 10, 11	syl331anc 1351	1 |- ( ph -> la )

Syntax hints:   -> wi 4   /\ 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:  eengtrkg  25865  ofscom  32114  cgrextend  32115  segconeq  32117  ifscgr  32151  cgrsub  32152  btwnxfr  32163  fscgr  32187  linecgr  32188  btwnconn1lem4  32197  btwnconn1lem5  32198  btwnconn1lem6  32199  btwnconn1lem8  32201  btwnconn1lem11  32204  seglecgr12  32218  colinbtwnle  32225  lshpkrlem6  34402  ps-2c  34814  pmodlem1  35132  pmodlem2  35133  dalawlem4  35160  dalawlem9  35165  4atexlemc  35355  cdleme11l  35556  cdleme15c  35563  cdleme16  35572  cdleme19e  35595  cdleme20l2  35609  cdleme20l  35610  cdleme20m  35611  cdleme20  35612  cdleme21d  35618  cdleme21e  35619  cdleme26ee  35648  cdleme26eALTN  35649  cdleme27a  35655  cdleme28b  35659  cdleme28c  35660  cdleme36m  35749  cdlemg12  35938  cdlemg16ALTN  35946  cdlemg17iqN  35962  cdlemg18c  35968  cdlemg19  35972  cdlemg21  35974  cdlemg28  35992  cdlemk11  36137  cdlemk12  36138  cdlemk16a  36144  cdlemk16  36145  cdlemk18  36156  cdlemk19  36157  cdlemk11u  36159  cdlemk12u  36160  cdlemk21N  36161  cdlemk20  36162  cdlemkoatnle-2N  36163  cdlemk13-2N  36164  cdlemkole-2N  36165  cdlemk14-2N  36166  cdlemk15-2N  36167  cdlemk16-2N  36168  cdlemk17-2N  36169  cdlemk18-2N  36174  cdlemk19-2N  36175  cdlemk7u-2N  36176  cdlemk11u-2N  36177  cdlemk12u-2N  36178  cdlemk22  36181  cdlemk30  36182  cdlemk23-3  36190  cdlemk26b-3  36193  cdlemk26-3  36194  cdlemk27-3  36195  cdlemk11ta  36217  cdlemk47  36237  dia2dimlem1  36353