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

Theorem syl121anc 1189
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1  |-  ( ph  ->  ps )
sylXanc.2  |-  ( ph  ->  ch )
sylXanc.3  |-  ( ph  ->  th )
sylXanc.4  |-  ( ph  ->  ta )
syl121anc.5  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
Assertion
Ref Expression
syl121anc  |-  ( ph  ->  et )

Proof of Theorem syl121anc
StepHypRef Expression
1 sylXanc.1 . 2  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
42, 3jca 519 . 2  |-  ( ph  ->  ( ch  /\  th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl121anc.5 . 2  |-  ( ( ps  /\  ( ch 
/\  th )  /\  ta )  ->  et )
71, 4, 5, 6syl3anc 1184 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl122anc  1193  disjxiun  4169  tfisi  4797  fsnunf2  5891  axdc4lem  8291  div32d  9769  div13d  9770  expdivd  11492  pcqmul  13182  pcid  13201  pcneg  13202  pc2dvds  13207  pcz  13209  pcaddlem  13212  pcadd  13213  pcmpt2  13217  pcbc  13224  qexpz  13225  expnprm  13226  spwpr4c  14619  sylow1lem1  15187  lspsneleq  16142  lspsneq  16149  lspfixed  16155  ucncn  18268  ucnextcn  18287  ssblex  18411  prdsxmslem2  18512  voliunlem1  19397  deg1mul3le  19992  deg1pw  19996  fta1blem  20044  bcmono  21014  dchrisum0flblem1  21155  dchrisum0flblem2  21156  pntibndlem1  21236  pntlemr  21249  0wlkon  21500  0pthon  21532  nv1  22118  measun  24518  measvuni  24521  measunl  24523  btwnconn1lem14  25938  segcon2  25943  seglelin  25954  neibastop3  26281  upixp  26321  fdc  26339  eldioph2b  26711  jm2.19lem4  26953  jm2.19  26954  jm2.26a  26961  jm2.26  26963  hbtlem2  27196  fnchoice  27567  stoweidlem42  27658  stoweidlem59  27675  eqlkr3  29584  lkrshp  29588  lfl1dim  29604  lfl1dim2N  29605  eqlkr4  29648  2llnneN  29891  3dim2  29950  4atlem3  30078  4atlem11  30091  4atlem12  30094  pexmidlem4N  30455  lhp2at0nle  30517  lhple  30524  ltrnideq  30657  cdlemd9  30688  cdleme0ex2N  30706  cdleme0moN  30707  cdleme11a  30742  cdleme30a  30860  cdlemefs32sn1aw  30896  cdleme43fsv1snlem  30902  cdlemefs31fv1  30906  cdlemefs45eN  30913  cdleme41sn3a  30915  cdleme35h  30938  cdleme36a  30942  cdleme40m  30949  cdleme40n  30950  cdleme41sn3aw  30956  cdleme42h  30964  cdleme42k  30966  cdleme42mN  30969  cdleme43cN  30973  cdleme17d3  30978  cdleme48fvg  30982  cdlemeg47rv2  30992  cdlemeg46c  30995  cdlemeg46sfg  31002  cdlemeg46rjgN  31004  cdlemeg46rgv  31010  cdlemeg46req  31011  cdlemeg46gfv  31012  cdlemeg46gfre  31014  cdlemeg49lebilem  31021  cdleme50trn2  31033  cdlemg2kq  31084  cdlemb3  31088  cdlemg4f  31097  cdlemg9a  31114  cdlemg9b  31115  cdlemg9  31116  cdlemg11aq  31120  cdlemg12a  31125  cdlemg12b  31126  cdlemg12c  31127  cdlemg12d  31128  cdlemg12f  31130  cdlemg12g  31131  cdlemg12  31132  cdlemg13a  31133  cdlemg16  31139  cdlemg17e  31147  cdlemg17f  31148  cdlemg17g  31149  cdlemg17ir  31152  cdlemg17  31159  cdlemg18b  31161  cdlemg18c  31162  cdlemg33e  31192  trlcoabs2N  31204  trlcocnvat  31206  trlcolem  31208  trlco  31209  cdlemg44  31215  cdlemg47  31218  ltrncom  31220  tendococl  31254  tendoplcl  31263  tendoplcom  31264  tendoplass  31265  tendodi1  31266  tendodi2  31267  tendo0pl  31273  tendoipl  31279  cdlemh1  31297  cdlemi2  31301  tendo0mul  31308  tendo0mulr  31309  cdlemk2  31314  cdlemk3  31315  cdlemk4  31316  cdlemk6  31319  cdlemk8  31320  cdlemk12  31332  cdlemkole  31335  cdlemk14  31336  cdlemk15  31337  cdlemk5u  31343  cdlemk6u  31344  cdlemk12u  31354  cdlemkfid1N  31403  cdlemk19x  31425  cdlemk48  31432  cdlemk53a  31437  cdlemk56  31453  cdleml2N  31459  cdleml3N  31460  cdleml6  31463  cdleml7  31464  dva1dim  31467  dia2dimlem4  31550  dvhlveclem  31591  doca2N  31609  djajN  31620  cdlemn2a  31679  cdlemn3  31680  dihordlem6  31696  dihord5apre  31745  dihglbcpreN  31783  dihmeetcN  31785  dihmeetbN  31786  dihmeetlem10N  31799  dihmeetlem12N  31801  dihmeetlem15N  31804  dihmeetALTN  31810  dih1dimatlem0  31811  dihjatcclem3  31903  dihjatcclem4  31904  mapdpglem22  32176  hdmap14lem1a  32352
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 178  df-an 361  df-3an 938
  Copyright terms: Public domain W3C validator