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

Theorem syl333anc 1251
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 1168 . 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 1244 1  |-  ( ph  ->  la )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 965
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 185  df-an 371  df-3an 967
This theorem is referenced by:  ofscom  28158  cgrextend  28159  segconeq  28161  ifscgr  28195  cgrsub  28196  btwnxfr  28207  fscgr  28231  linecgr  28232  btwnconn1lem4  28241  btwnconn1lem5  28242  btwnconn1lem6  28243  btwnconn1lem8  28245  btwnconn1lem11  28248  seglecgr12  28262  colinbtwnle  28269  lshpkrlem6  33042  ps-2c  33454  pmodlem1  33772  pmodlem2  33773  dalawlem4  33800  dalawlem9  33805  4atexlemc  33995  cdleme11l  34195  cdleme15c  34202  cdleme16  34211  cdleme19e  34233  cdleme20l2  34247  cdleme20l  34248  cdleme20m  34249  cdleme20  34250  cdleme21d  34256  cdleme21e  34257  cdleme26ee  34286  cdleme26eALTN  34287  cdleme27a  34293  cdleme28b  34297  cdleme28c  34298  cdleme36m  34387  cdlemg12  34576  cdlemg16ALTN  34584  cdlemg17iqN  34600  cdlemg18c  34606  cdlemg19  34610  cdlemg21  34612  cdlemg28  34630  cdlemk11  34775  cdlemk12  34776  cdlemk16a  34782  cdlemk16  34783  cdlemk18  34794  cdlemk19  34795  cdlemk11u  34797  cdlemk12u  34798  cdlemk21N  34799  cdlemk20  34800  cdlemkoatnle-2N  34801  cdlemk13-2N  34802  cdlemkole-2N  34803  cdlemk14-2N  34804  cdlemk15-2N  34805  cdlemk16-2N  34806  cdlemk17-2N  34807  cdlemk18-2N  34812  cdlemk19-2N  34813  cdlemk7u-2N  34814  cdlemk11u-2N  34815  cdlemk12u-2N  34816  cdlemk22  34819  cdlemk30  34820  cdlemk23-3  34828  cdlemk26b-3  34831  cdlemk26-3  34832  cdlemk27-3  34833  cdlemk11ta  34855  cdlemk47  34875  dia2dimlem1  34991
  Copyright terms: Public domain W3C validator