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  24630  cgrextend  24631  segconeq  24633  ifscgr  24667  cgrsub  24668  btwnxfr  24679  fscgr  24703  linecgr  24704  btwnconn1lem4  24713  btwnconn1lem5  24714  btwnconn1lem6  24715  btwnconn1lem8  24717  btwnconn1lem11  24720  seglecgr12  24734  colinbtwnle  24741  lshpkrlem6  29305  ps-2c  29717  pmodlem1  30035  pmodlem2  30036  dalawlem4  30063  dalawlem9  30068  4atexlemc  30258  cdleme11l  30458  cdleme15c  30465  cdleme16  30474  cdleme19e  30496  cdleme20l2  30510  cdleme20l  30511  cdleme20m  30512  cdleme20  30513  cdleme21d  30519  cdleme21e  30520  cdleme26ee  30549  cdleme26eALTN  30550  cdleme27a  30556  cdleme28b  30560  cdleme28c  30561  cdleme36m  30650  cdlemg12  30839  cdlemg16ALTN  30847  cdlemg17iqN  30863  cdlemg18c  30869  cdlemg19  30873  cdlemg21  30875  cdlemg28  30893  cdlemk11  31038  cdlemk12  31039  cdlemk16a  31045  cdlemk16  31046  cdlemk18  31057  cdlemk19  31058  cdlemk11u  31060  cdlemk12u  31061  cdlemk21N  31062  cdlemk20  31063  cdlemkoatnle-2N  31064  cdlemk13-2N  31065  cdlemkole-2N  31066  cdlemk14-2N  31067  cdlemk15-2N  31068  cdlemk16-2N  31069  cdlemk17-2N  31070  cdlemk18-2N  31075  cdlemk19-2N  31076  cdlemk7u-2N  31077  cdlemk11u-2N  31078  cdlemk12u-2N  31079  cdlemk22  31082  cdlemk30  31083  cdlemk23-3  31091  cdlemk26b-3  31094  cdlemk26-3  31095  cdlemk27-3  31096  cdlemk11ta  31118  cdlemk47  31138  dia2dimlem1  31254
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