MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl333anc Unicode version

Theorem syl333anc 1214
Description: A syllogism inference combined with contraction. (Contributed by NM, 10-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
sylXanc.5  |-  ( ph  ->  et )
sylXanc.6  |-  ( ph  ->  ze )
sylXanc.7  |-  ( ph  ->  si )
sylXanc.8  |-  ( ph  ->  rh )
sylXanc.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
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . 2  |-  ( ph  ->  ch )
3 sylXanc.3 . 2  |-  ( ph  ->  th )
4 sylXanc.4 . 2  |-  ( ph  ->  ta )
5 sylXanc.5 . 2  |-  ( ph  ->  et )
6 sylXanc.6 . 2  |-  ( ph  ->  ze )
7 sylXanc.7 . . 3  |-  ( ph  ->  si )
8 sylXanc.8 . . 3  |-  ( ph  ->  rh )
9 sylXanc.9 . . 3  |-  ( ph  ->  mu )
107, 8, 93jca 1132 . 2  |-  ( ph  ->  ( si  /\  rh  /\  mu ) )
11 syl333anc.10 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ( ta  /\  et  /\  ze )  /\  ( si  /\  rh  /\  mu ) )  ->  la )
121, 2, 3, 4, 5, 6, 10, 11syl331anc 1207 1  |-  ( ph  ->  la )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  ofscom  25016  cgrextend  25017  segconeq  25019  ifscgr  25053  cgrsub  25054  btwnxfr  25065  fscgr  25089  linecgr  25090  btwnconn1lem4  25099  btwnconn1lem5  25100  btwnconn1lem6  25101  btwnconn1lem8  25103  btwnconn1lem11  25106  seglecgr12  25120  colinbtwnle  25127  lshpkrlem6  29123  ps-2c  29535  pmodlem1  29853  pmodlem2  29854  dalawlem4  29881  dalawlem9  29886  4atexlemc  30076  cdleme11l  30276  cdleme15c  30283  cdleme16  30292  cdleme19e  30314  cdleme20l2  30328  cdleme20l  30329  cdleme20m  30330  cdleme20  30331  cdleme21d  30337  cdleme21e  30338  cdleme26ee  30367  cdleme26eALTN  30368  cdleme27a  30374  cdleme28b  30378  cdleme28c  30379  cdleme36m  30468  cdlemg12  30657  cdlemg16ALTN  30665  cdlemg17iqN  30681  cdlemg18c  30687  cdlemg19  30691  cdlemg21  30693  cdlemg28  30711  cdlemk11  30856  cdlemk12  30857  cdlemk16a  30863  cdlemk16  30864  cdlemk18  30875  cdlemk19  30876  cdlemk11u  30878  cdlemk12u  30879  cdlemk21N  30880  cdlemk20  30881  cdlemkoatnle-2N  30882  cdlemk13-2N  30883  cdlemkole-2N  30884  cdlemk14-2N  30885  cdlemk15-2N  30886  cdlemk16-2N  30887  cdlemk17-2N  30888  cdlemk18-2N  30893  cdlemk19-2N  30894  cdlemk7u-2N  30895  cdlemk11u-2N  30896  cdlemk12u-2N  30897  cdlemk22  30900  cdlemk30  30901  cdlemk23-3  30909  cdlemk26b-3  30912  cdlemk26-3  30913  cdlemk27-3  30914  cdlemk11ta  30936  cdlemk47  30956  dia2dimlem1  31072
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator