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

Theorem syl31anc 1231
Description: Syllogism combined with contraction. (Contributed by NM, 11-Mar-2012.)
Hypotheses
Ref Expression
sylXanc.1
sylXanc.2
sylXanc.3
sylXanc.4
syl31anc.5
Assertion
Ref Expression
syl31anc

Proof of Theorem syl31anc
StepHypRef Expression
1 sylXanc.1 . . 3
2 sylXanc.2 . . 3
3 sylXanc.3 . . 3
41, 2, 33jca 1176 . 2
5 sylXanc.4 . 2
6 syl31anc.5 . 2
74, 5, 6syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  /\w3a 973
This theorem is referenced by:  syl32anc  1236  stoic4b  1611  elovmpt3rab1  6536  smo11  7054  omeulem2  7251  oeeui  7270  oaabs2  7313  omabs  7315  omxpenlem  7638  map2xp  7707  mapdom2  7708  fsuppsssupp  7865  cantnflt  8112  cantnfltOLD  8142  cnfcom  8165  cnfcomOLD  8173  mapcdaen  8585  pwsdompw  8605  cofsmo  8670  fin1a2lem4  8804  ltmul12a  10423  lt2msq1  10453  ledivp1  10472  lemul1ad  10510  lemul2ad  10511  supmul1  10533  supmul  10536  rpnnen1lem3  11239  rpnnen1lem5  11241  lediv2ad  11307  xaddge0  11479  xadddi  11516  xadddi2  11518  supicc  11697  supiccub  11698  supicclub  11699  difelfznle  11818  flval3  11951  modidmul0  12022  fseqsupubi  12088  expcan  12218  ltexp2  12219  ltexp2r  12222  expubnd  12226  ltexp2rd  12334  ltexp2d  12339  leexp2d  12340  expcand  12341  swrdid  12652  swrd0fv  12666  swrds1  12676  ccatswrd  12681  swrdccat2  12683  swrdccatin2  12712  swrdccatin12lem2  12714  swrdccatin12lem3  12715  splfv1  12731  cshwidxmod  12774  o1fsum  13627  mertenslem1  13693  eftlub  13844  rpnnen2lem4  13951  ruclem12  13974  dvdsadd  14024  3dvds  14050  divalgmod  14064  bitsmod  14086  bitsinv1lem  14091  bezoutlem4  14179  gcdeq  14190  rplpwr  14194  sqgcd  14196  rpmulgcd2  14246  isprm5  14253  divgcdodd  14260  rpdvds  14265  divnumden  14281  crt  14308  phimullem  14309  modprm0  14330  modprmn0modprm0  14332  coprimeprodsq2  14334  pythagtriplem19  14357  pockthlem  14423  prmunb  14432  prmreclem3  14436  prmreclem6  14439  ramub  14531  ramz  14543  pmtrprfv  16478  pmtrprfv3  16479  mndodcong  16566  odngen  16597  pgpfi  16625  pgpssslw  16634  sylow2blem3  16642  lsmless1  16679  lsmless2  16680  lsmless12  16681  lsmmod2  16694  pj1id  16717  odadd2  16855  gexexlem  16858  ablfacrplem  17116  ablfacrp  17117  ablfac1b  17121  ablfac1eu  17124  pgpfac1lem2  17126  kerf1hrm  17392  lsmssspx  17734  lspsncv0  17792  coe1subfv  18307  coe1fzgsumdlem  18343  znunit  18602  uvcvvcl2  18819  uvcvv1  18820  uvcvv0  18821  scmate  19012  mdetunilem2  19115  pmatcoe1fsupp  19202  mat2pmatlin  19236  decpmatmullem  19272  pmatcollpw1lem1  19275  pmatcollpw1lem2  19276  pm2mpghm  19317  chpscmat  19343  chp0mat  19347  chpidmat  19348  cpmadugsumlemB  19375  cpmadugsumlemC  19376  cpmadugsumlemF  19377  clsndisj  19576  neiptopnei  19633  rnelfm  20454  fmfnfmlem2  20456  fmfnfm  20459  flimss1  20474  isfcf  20535  cnextfun  20564  cnextfvval  20565  cnextf  20566  cnextcn  20567  cnextfres  20568  ustuqtop1  20744  utopsnneiplem  20750  xblss2ps  20904  xblss2  20905  stdbdxmet  21018  metcnpi3  21049  metustexhalfOLD  21066  metustexhalf  21067  nmoi  21235  nmoi2  21237  nmoco  21244  blcvx  21303  icccmplem2  21328  icccmplem3  21329  reconnlem2  21332  xrge0gsumle  21338  metds0  21354  metdstri  21355  metdseq0  21358  lebnumlem3  21463  nmoleub2lem  21597  bcthlem5  21767  minveclem2  21841  minveclem3b  21843  minveclem4  21847  minveclem6  21849  icombl  21974  cncombf  22065  mbflimsup  22073  itg2monolem1  22157  itg2mono  22160  itg2cnlem1  22168  itg2cnlem2  22169  bddmulibl  22245  ellimc2  22281  cpnord  22338  cpnres  22340  dvmulbr  22342  dvcobr  22349  dvlipcn  22395  dvlip2  22396  c1liplem1  22397  dvivthlem1  22409  lhop1lem  22414  lhop1  22415  dvfsumlem2  22428  itgsubstlem  22449  deg1add  22504  deg1sublt  22511  ply1remlem  22563  plyeq0lem  22607  taylthlem2  22769  ulmdvlem3  22797  abelthlem7  22833  pilem2  22847  pilem3  22848  pige3  22910  logccv  23044  cxpaddlelem  23125  cvxcl  23314  fsumharmonic  23341  ftalem5  23350  dvdsdivcl  23457  dvdsmulf1o  23470  bposlem1  23559  lgsqr  23621  lgsquad2lem2  23634  2sqlem8a  23646  2sqlem8  23647  dchrmusum2  23679  dchrvmasumiflem1  23686  dchrisum0flblem1  23693  dchrisum0lem1b  23700  pntlem3  23794  tgdim01  23898  axsegcon  24230  ax5seglem1  24231  ax5seglem2  24232  axlowdimlem6  24250  axeuclidlem  24265  axcontlem7  24273  axcontlem9  24275  axcontlem10  24276  cusgrasize2inds  24477  usgra2adedgspth  24613  vdgrun  24901  vdgrfiun  24902  vdgr1d  24903  vdgr1b  24904  vdgr1a  24906  2pthfrgra  25011  vdn1frgrav2  25025  vdgn1frgrav2  25026  frgrawopreg  25049  frrusgraord  25071  numclwwlk2lem1  25102  numclwwlk3  25109  frgrareg  25117  nmoub3i  25688  ubthlem3  25788  minvecolem2  25791  minvecolem4  25796  minvecolem5  25797  minvecolem6  25798  htthlem  25834  pjpjpre  26337  chscllem1  26555  chscllem2  26556  chscllem3  26557  cnlnadjlem2  26987  leopnmid  27057  br8d  27463  ogrpaddlt  27708  archirngz  27733  ornglmullt  27797  orngrmullt  27798  elrhmunit  27810  qqhval2lem  27962  qqhnm  27971  qqhucn  27973  esumcst  28071  esumpcvgval  28084  measunl  28187  dya2iocbrsiga  28246  dya2icobrsiga  28247  sibfof  28282  oddpwdc  28293  eulerpartlemgc  28301  bayesth  28378  erdszelem8  28642  br8  29185  supaddc  30041  supadd  30042  totbndbnd  30285  prdsbnd  30289  rrncmslem  30328  rrntotbnd  30332  isdrngo2  30361  mzpsubst  30681  rencldnfi  30755  irrapx1  30764  pellexlem3  30767  pellexlem5  30769  infmrgelbi  30814  pellqrex  30815  pellfundge  30818  rmspecfund  30845  congtr  30903  acongeq  30921  bezoutr  30923  jm2.20nn  30939  jm2.25lem1  30940  jm2.26  30944  expdiophlem1  30963  hbtlem2  31073  suprnmpt  31451  upbdrech  31505  ssfiunibd  31509  iccintsng  31563  limcrecl  31635  dvmulcncf  31722  dvdivcncf  31724  dvbdfbdioolem1  31725  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  stoweidlem1  31783  stoweidlem20  31802  stoweidlem24  31806  stoweidlem34  31816  stoweidlem45  31827  stoweidlem60  31842  fourierdlem20  31909  fourierdlem31  31920  fourierdlem38  31927  fourierdlem64  31953  fourierdlem79  31968  fourierdlem94  31983  fourierdlem113  32002  fouriersw  32014  fouriercn  32015  lincresunit3  33082  lsatcmp  34728  lcvexchlem2  34760  lcvexchlem3  34761  ncvr1  34997  cvrletrN  34998  cvrnbtwn3  35001  cvrnrefN  35007  cvrcmp  35008  0ltat  35016  atnle0  35034  atlen0  35035  cvlcvr1  35064  cvrval3  35137  atle  35160  athgt  35180  1cvratex  35197  ps-2  35202  ps-2b  35206  llnnleat  35237  2atneat  35239  llnle  35242  atcvrlln  35244  llncmp  35246  2llnmat  35248  2at0mat0  35249  2atm  35251  ps-2c  35252  lplnle  35264  lplnnle2at  35265  llncvrlpln2  35281  llncvrlpln  35282  2lplnmN  35283  2llnmj  35284  2atmat  35285  lplncmp  35286  lplnexllnN  35288  2llnm2N  35292  2llnm4  35294  lvolnle3at  35306  4atlem3a  35321  4atlem3b  35322  4atlem10  35330  4atlem11  35333  4atlem12  35336  lplncvrlvol2  35339  lplncvrlvol  35340  lvolcmp  35341  2lplnm2N  35345  2lplnmj  35346  dalempjsen  35377  dalemcea  35384  dalem2  35385  dalemdea  35386  dalem9  35396  dalem16  35403  dalemcjden  35416  dalem21  35418  dalem23  35420  dalem39  35435  dalem54  35450  dalem60  35456  cdlemb  35518  elpadd2at  35530  paddasslem4  35547  paddasslem7  35550  paddasslem15  35558  paddasslem16  35559  pmodlem1  35570  pmodlem2  35571  llnexchb2  35593  pclfinclN  35674  osumcllem9N  35688  pmapojoinN  35692  pexmidN  35693  pl42lem1N  35703  lhp0lt  35727  lhpexle1  35732  lhpexle2lem  35733  lhpexle3lem  35735  lhprelat3N  35764  ltrnid  35859  trlval3  35912  arglem1N  35915  cdlemc5  35920  cdleme3b  35954  cdleme3c  35955  cdleme3h  35960  cdleme7e  35972  cdleme7ga  35973  cdleme20l1  36046  cdleme20l2  36047  cdleme20l  36048  cdleme22b  36067  cdlemefrs29clN  36125  cdlemefrs32fva  36126  cdlemeg46fvcl  36232  cdlemeg46c  36239  cdlemeg46fvaw  36242  cdlemeg46req  36255  cdleme48fgv  36264  cdlemf1  36287  cdlemg1cex  36314  cdlemg2dN  36316  cdlemg2ce  36318  cdlemg12e  36373  cdlemg35  36439  cdlemh  36543  tendocan  36550  cdlemk28-3  36634  tendoex  36701  dih1  37013  dihmeetlem9N  37042  dihlspsnssN  37059  dihlspsnat  37060  lcfrlem23  37292  suprubd  37976  suprleubrd  37983  suprlubrd  37987
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
  Copyright terms: Public domain W3C validator