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

Theorem syl333anc 1260
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 1176 . 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 1253 1  |-  ( ph  ->  la )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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 975
This theorem is referenced by:  ofscom  29234  cgrextend  29235  segconeq  29237  ifscgr  29271  cgrsub  29272  btwnxfr  29283  fscgr  29307  linecgr  29308  btwnconn1lem4  29317  btwnconn1lem5  29318  btwnconn1lem6  29319  btwnconn1lem8  29321  btwnconn1lem11  29324  seglecgr12  29338  colinbtwnle  29345  lshpkrlem6  33912  ps-2c  34324  pmodlem1  34642  pmodlem2  34643  dalawlem4  34670  dalawlem9  34675  4atexlemc  34865  cdleme11l  35065  cdleme15c  35072  cdleme16  35081  cdleme19e  35103  cdleme20l2  35117  cdleme20l  35118  cdleme20m  35119  cdleme20  35120  cdleme21d  35126  cdleme21e  35127  cdleme26ee  35156  cdleme26eALTN  35157  cdleme27a  35163  cdleme28b  35167  cdleme28c  35168  cdleme36m  35257  cdlemg12  35446  cdlemg16ALTN  35454  cdlemg17iqN  35470  cdlemg18c  35476  cdlemg19  35480  cdlemg21  35482  cdlemg28  35500  cdlemk11  35645  cdlemk12  35646  cdlemk16a  35652  cdlemk16  35653  cdlemk18  35664  cdlemk19  35665  cdlemk11u  35667  cdlemk12u  35668  cdlemk21N  35669  cdlemk20  35670  cdlemkoatnle-2N  35671  cdlemk13-2N  35672  cdlemkole-2N  35673  cdlemk14-2N  35674  cdlemk15-2N  35675  cdlemk16-2N  35676  cdlemk17-2N  35677  cdlemk18-2N  35682  cdlemk19-2N  35683  cdlemk7u-2N  35684  cdlemk11u-2N  35685  cdlemk12u-2N  35686  cdlemk22  35689  cdlemk30  35690  cdlemk23-3  35698  cdlemk26b-3  35701  cdlemk26-3  35702  cdlemk27-3  35703  cdlemk11ta  35725  cdlemk47  35745  dia2dimlem1  35861
  Copyright terms: Public domain W3C validator