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

Theorem syl31anc 1187
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 )
syl31anc.5  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
Assertion
Ref Expression
syl31anc  |-  ( ph  ->  et )

Proof of Theorem syl31anc
StepHypRef Expression
1 sylXanc.1 . . 3  |-  ( ph  ->  ps )
2 sylXanc.2 . . 3  |-  ( ph  ->  ch )
3 sylXanc.3 . . 3  |-  ( ph  ->  th )
41, 2, 33jca 1134 . 2  |-  ( ph  ->  ( ps  /\  ch  /\ 
th ) )
5 sylXanc.4 . 2  |-  ( ph  ->  ta )
6 syl31anc.5 . 2  |-  ( ( ( ps  /\  ch  /\ 
th )  /\  ta )  ->  et )
74, 5, 6syl2anc 643 1  |-  ( ph  ->  et )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    /\ w3a 936
This theorem is referenced by:  syl32anc  1192  smo11  6585  omeulem2  6785  oeeui  6804  oaabs2  6847  omabs  6849  omxpenlem  7168  map2xp  7236  mapdom2  7237  cantnflt  7583  cnfcom  7613  mapcdaen  8020  pwsdompw  8040  cofsmo  8105  fin1a2lem4  8239  ltmul12a  9822  lt2msq1  9849  ledivp1  9868  lemul1ad  9906  lemul2ad  9907  supmul1  9929  supmul  9932  rpnnen1lem3  10558  rpnnen1lem5  10560  lediv2ad  10626  xaddge0  10793  xadddi  10830  xadddi2  10832  flval3  11177  fseqsupubi  11272  expcan  11387  ltexp2  11388  ltexp2r  11391  expubnd  11395  ltexp2rd  11502  ltexp2d  11507  leexp2d  11508  expcand  11509  swrdid  11727  ccatswrd  11728  swrdccat2  11730  splfv1  11739  swrds1  11742  o1fsum  12547  mertenslem1  12616  eftlub  12665  rpnnen2lem4  12772  ruclem12  12795  dvdsadd  12843  3dvds  12867  divalgmod  12881  bitsmod  12903  bitsinv1lem  12908  bezoutlem4  12996  gcdeq  13007  rplpwr  13011  sqgcd  13013  rpmulgcd2  13060  isprm5  13067  divgcdodd  13074  rpdvds  13079  divnumden  13095  crt  13122  phimullem  13123  coprimeprodsq2  13139  pythagtriplem19  13162  pockthlem  13228  prmunb  13237  prmreclem3  13241  prmreclem6  13244  ramub  13336  ramz  13348  mndodcong  15135  odngen  15166  pgpfi  15194  pgpssslw  15203  sylow2blem3  15211  lsmless1  15248  lsmless2  15249  lsmless12  15250  lsmmod2  15263  pj1id  15286  odadd2  15419  gexexlem  15422  ablfacrplem  15578  ablfacrp  15579  ablfac1b  15583  ablfac1eu  15586  pgpfac1lem2  15588  lsmssspx  16115  lspsncv0  16173  coe1subfv  16614  znunit  16799  clsndisj  17094  neiptopnei  17151  rnelfm  17938  fmfnfmlem2  17940  fmfnfm  17943  flimss1  17958  isfcf  18019  cnextfun  18048  cnextfvval  18049  cnextf  18050  cnextcn  18051  cnextfres  18052  ustuqtop1  18224  utopsnneiplem  18230  xblss2ps  18384  xblss2  18385  stdbdxmet  18498  metcnpi3  18529  metustexhalfOLD  18546  metustexhalf  18547  nmoi  18715  nmoi2  18717  nmoco  18724  blcvx  18782  icccmplem2  18807  icccmplem3  18808  reconnlem2  18811  xrge0gsumle  18817  metds0  18833  metdstri  18834  metdseq0  18837  lebnumlem3  18941  nmoleub2lem  19075  bcthlem5  19234  minveclem2  19280  minveclem3b  19282  minveclem4  19286  minveclem6  19288  icombl  19411  cncombf  19503  mbflimsup  19511  itg2monolem1  19595  itg2mono  19598  itg2cnlem1  19606  itg2cnlem2  19607  bddmulibl  19683  ellimc2  19717  cpnord  19774  cpnres  19776  dvmulbr  19778  dvcobr  19785  dvlipcn  19831  dvlip2  19832  c1liplem1  19833  dvivthlem1  19845  lhop1lem  19850  lhop1  19851  dvfsumlem2  19864  itgsubstlem  19885  deg1add  19979  deg1sublt  19986  ply1remlem  20038  plyeq0lem  20082  taylthlem2  20243  ulmdvlem3  20271  abelthlem7  20307  pilem2  20321  pilem3  20322  pige3  20378  logccv  20507  cxpaddlelem  20588  cvxcl  20776  fsumharmonic  20803  ftalem5  20812  dvdsdivcl  20919  dvdsmulf1o  20932  bposlem1  21021  lgsqr  21083  lgsquad2lem2  21096  2sqlem8a  21108  2sqlem8  21109  dchrmusum2  21141  dchrvmasumiflem1  21148  dchrisum0flblem1  21155  dchrisum0lem1b  21162  pntlem3  21256  cusgrasize2inds  21439  vdgrun  21625  vdgrfiun  21626  vdgr1d  21627  vdgr1b  21628  vdgr1a  21630  nmoub3i  22227  ubthlem3  22327  minvecolem2  22330  minvecolem4  22335  minvecolem5  22336  minvecolem6  22337  htthlem  22373  pjpjpre  22874  chscllem1  23092  chscllem2  23093  chscllem3  23094  cnlnadjlem2  23524  leopnmid  23594  ofldaddlt  24194  elrhmunit  24211  kerf1hrm  24215  qqhval2lem  24318  qqhnm  24327  qqhucn  24329  esumcst  24408  esumpcvgval  24421  measunl  24523  dya2iocbrsiga  24578  dya2icobrsiga  24579  bayesth  24650  erdszelem8  24837  br8  25327  axsegcon  25770  ax5seglem1  25771  ax5seglem2  25772  axlowdimlem6  25790  axeuclidlem  25805  axcontlem7  25813  axcontlem9  25815  axcontlem10  25816  supaddc  26137  supadd  26138  areacirclem3  26182  totbndbnd  26388  prdsbnd  26392  rrncmslem  26431  rrntotbnd  26435  isdrngo2  26464  mzpsubst  26695  rencldnfi  26772  irrapx1  26781  pellexlem3  26784  pellexlem5  26786  infmrgelbi  26831  pellqrex  26832  pellfundge  26835  rmspecfund  26862  congtr  26920  acongeq  26938  bezoutr  26940  jm2.20nn  26958  jm2.25lem1  26959  jm2.26  26963  expdiophlem1  26982  uvcvvcl2  27105  uvcvv1  27106  uvcvv0  27107  hbtlem2  27196  pmtrprfv  27264  stoweidlem1  27617  stoweidlem24  27640  stoweidlem34  27650  stoweidlem45  27661  stoweidlem60  27676  swrdccatin2  28018  swrdccatin12lem3  28024  swrdccatin12lem4  28025  usgra2adedgspth  28045  2pthfrgra  28115  vdn1frgrav2  28130  vdgn1frgrav2  28131  frgrawopreg  28152  lsatcmp  29486  lcvexchlem2  29518  lcvexchlem3  29519  ncvr1  29755  cvrletrN  29756  cvrnbtwn3  29759  cvrnrefN  29765  cvrcmp  29766  0ltat  29774  atnle0  29792  atlen0  29793  cvlcvr1  29822  cvrval3  29895  atle  29918  athgt  29938  1cvratex  29955  ps-2  29960  ps-2b  29964  llnnleat  29995  2atneat  29997  llnle  30000  atcvrlln  30002  llncmp  30004  2llnmat  30006  2at0mat0  30007  2atm  30009  ps-2c  30010  lplnle  30022  lplnnle2at  30023  llncvrlpln2  30039  llncvrlpln  30040  2lplnmN  30041  2llnmj  30042  2atmat  30043  lplncmp  30044  lplnexllnN  30046  2llnm2N  30050  2llnm4  30052  lvolnle3at  30064  4atlem3a  30079  4atlem3b  30080  4atlem10  30088  4atlem11  30091  4atlem12  30094  lplncvrlvol2  30097  lplncvrlvol  30098  lvolcmp  30099  2lplnm2N  30103  2lplnmj  30104  dalempjsen  30135  dalemcea  30142  dalem2  30143  dalemdea  30144  dalem9  30154  dalem16  30161  dalemcjden  30174  dalem21  30176  dalem23  30178  dalem39  30193  dalem54  30208  dalem60  30214  cdlemb  30276  elpadd2at  30288  paddasslem4  30305  paddasslem7  30308  paddasslem15  30316  paddasslem16  30317  pmodlem1  30328  pmodlem2  30329  llnexchb2  30351  pclfinclN  30432  osumcllem9N  30446  pmapojoinN  30450  pexmidN  30451  pl42lem1N  30461  lhp0lt  30485  lhpexle1  30490  lhpexle2lem  30491  lhpexle3lem  30493  lhprelat3N  30522  ltrnid  30617  trlval3  30669  arglem1N  30672  cdlemc5  30677  cdleme3b  30711  cdleme3c  30712  cdleme3h  30717  cdleme7e  30729  cdleme7ga  30730  cdleme20l1  30802  cdleme20l2  30803  cdleme20l  30804  cdleme22b  30823  cdlemefrs29clN  30881  cdlemefrs32fva  30882  cdlemeg46fvcl  30988  cdlemeg46c  30995  cdlemeg46fvaw  30998  cdlemeg46req  31011  cdleme48fgv  31020  cdlemf1  31043  cdlemg1cex  31070  cdlemg2dN  31072  cdlemg2ce  31074  cdlemg12e  31129  cdlemg35  31195  cdlemh  31299  tendocan  31306  cdlemk28-3  31390  tendoex  31457  dih1  31769  dihmeetlem9N  31798  dihlspsnssN  31815  dihlspsnat  31816  lcfrlem23  32048
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