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

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

Proof of Theorem syl22anc
StepHypRef Expression
1 sylXanc.1 . . 3
2 sylXanc.2 . . 3
31, 2jca 532 . 2
4 sylXanc.3 . 2
5 sylXanc.4 . 2
6 syl22anc.5 . 2
73, 4, 5, 6syl12anc 1226 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  fr2nr  4862  soltmin  5411  f1oprg  5861  fveqf1o  6205  weniso  6250  fr3nr  6615  smogt  7057  smorndom  7058  oacomf1o  7233  difsnen  7619  undom  7625  enfixsn  7646  domss2  7696  ssenen  7711  marypha1lem  7913  fisupcl  7948  ordtypelem3  7966  ordtypelem8  7971  oieu  7985  oismo  7986  wofib  7991  wemaplem2  7993  wemapso  7997  wemapso2OLD  7998  wemapso2lem  7999  unxpwdom2  8035  infdifsn  8094  oemapvali  8124  cantnflem1c  8127  cantnflem1  8129  cantnf  8133  cantnfOLD  8155  cnfcom3  8169  cnfcom3OLD  8177  r1ordg  8217  dif1card  8409  infxpenlem  8412  dfac8clem  8434  infxp  8616  infmap2  8619  cflim2  8664  coftr  8674  fin2i2  8719  enfin2i  8722  fin23lem26  8726  fin23lem27  8729  fin23lem40  8752  isf32lem2  8755  isf32lem3  8756  isf32lem4  8757  isf32lem7  8760  isf32lem9  8762  fin1a2lem13  8813  fin12  8814  alephexp1  8975  gchdomtri  9028  fpwwe2lem12  9040  fpwwe2lem13  9041  gchpwdom  9069  gchhar  9078  adderpqlem  9353  mulerpqlem  9354  addassnq  9357  mulassnq  9358  distrnq  9360  mulidnq  9362  recmulnq  9363  ltexnq  9374  distrlem1pr  9424  distrlem4pr  9425  prlem936  9446  reclem3pr  9448  mulcmpblnr  9469  mulgt0d  9758  mul4d  9813  add4d  9826  add42d  9827  subcan  9897  addsub4d  10001  subadd4d  10002  sub4d  10003  2addsubd  10004  addsubeq4d  10005  muladdd  10039  mulsubd  10040  addgegt0d  10151  addge0d  10153  mulge0d  10154  le2addd  10195  le2subd  10196  ltleaddd  10197  leltaddd  10198  lt2subd  10200  divdivdiv  10270  divcan5  10271  divne0d  10361  recdivd  10362  recdiv2d  10363  divcan6d  10364  ddcand  10365  rec11d  10366  divmuldivd  10386  divmul13d  10387  divmul24d  10388  divadddivd  10389  divsubdivd  10390  divmuleqd  10391  divdivdivd  10392  subrecd  10400  mulge0b  10437  recreclt  10469  divgt0d  10506  mulgt1d  10507  lemulge11d  10508  lemulge12d  10509  ltmul12ad  10512  lemul12ad  10513  lemul12bd  10514  supmul1  10533  nndivtr  10602  qreccl  11231  ledivdivd  11310  lediv12ad  11340  lt2mul2divd  11343  xlt2add  11481  supxrun  11536  supxrre  11548  infmxrre  11556  iccss2  11624  iccssico2  11627  lincmb01cmp  11692  iccf1o  11693  fzrev2i  11773  modaddmodup  12050  modaddmodlo  12051  modsubdir  12055  fzennn  12078  sermono  12139  mulexpz  12206  expaddz  12210  ltexp2a  12217  leexp2a  12221  sqdiv  12233  expmulnbnd  12298  digit1  12300  expsubd  12321  lt2sqd  12344  le2sqd  12345  sq11d  12346  bcm1k  12393  bcp1n  12394  bcp1nk  12395  hashf1lem1  12504  cshw1  12790  2swrd2eqwrdeq  12891  absrele  13141  sqreulem  13192  sqrtmuld  13256  sqrtsq2d  13257  sqrtled  13258  sqrtltd  13259  sqr11d  13260  abs3lemd  13292  rlimuni  13373  climuni  13375  lo1resb  13387  o1resb  13389  2clim  13395  addcn2  13416  mulcn2  13418  o1of2  13435  o1rlimmul  13441  lo1add  13449  lo1mul  13450  isercolllem1  13487  caucvgrlem  13495  iseraltlem2  13505  iseraltlem3  13506  iseralt  13507  mptfzshft  13593  fsumrev  13594  fsum0diag2  13598  binomlem  13641  climcndslem1  13661  climcndslem2  13662  harmonic  13670  mertenslem1  13693  fprodser  13756  fprodrev  13781  efcllem  13813  moddvds  13993  dvds1  14034  dvdsext  14037  oexpneg  14049  bitsinv1  14092  sadaddlem  14116  sadasslem  14120  sadeq  14122  mulgcd  14184  dvdssqlem  14197  rpmulgcd2  14246  isprm6  14250  isprm5  14253  crt  14308  eulerthlem2  14312  prmdiveq  14316  pythagtriplem11  14349  pythagtriplem13  14351  iserodd  14359  pcgcd1  14400  pcprmpw2  14405  pcaddlem  14407  fldivp1  14416  4sqlem12  14474  4sqlem14  14476  4sqlem15  14477  4sqlem16  14478  vdwapun  14492  mreexexlem4d  15044  acsfn1  15058  acsfn2  15060  sscpwex  15184  rescabs  15202  yonedainv  15550  subm0  15987  pmtrfb  16490  psgnunilem1  16518  odmodnn0  16564  odeq  16574  dfod2  16586  sylow1lem1  16618  lsmsubg  16674  lsmmod  16693  lsmdisj2  16700  ghmplusg  16852  odadd  16856  gexexlem  16858  lt6abl  16897  cyggex2  16899  dprdfinv  17059  dmdprdsplitlem  17084  dpjidcl  17107  ablfacrp  17117  ablfacrp2  17118  ablfac1c  17122  ablfac1eu  17124  lcomfsupOLD  17549  lcomfsupp  17550  lssvancl1  17591  lssvnegcl  17602  lspprvacl  17645  lspsneli  17647  lspsn  17648  lmhmplusg  17690  lmhmima  17693  lmhmpreima  17694  reslmhm  17698  lbsind2  17727  lsmcl  17729  lsmelval2  17731  lsppreli  17736  lspprabs  17741  pj1lmhm  17746  lssvs0or  17756  lspabs3  17767  lspfixed  17774  lspexch  17775  lsmcv  17787  lspsolv  17789  lidlmcl  17865  drngnidl  17877  2idlcpbl  17882  mplbas2  18134  mplbas2OLD  18135  evlslem3  18183  evlslem1  18184  coe1addfv  18306  lply1binom  18348  evl1addd  18377  evl1subd  18378  evl1muld  18379  gzrngunit  18483  zringlpirlem3  18511  zlpirlem3  18516  prmirredlem  18523  prmirredlemOLD  18526  znf1o  18590  znunithash  18603  frlmsubgval  18798  frlmvscaval  18800  frlmphllem  18811  frlmphl  18812  frlmssuvc1  18825  frlmssuvc1OLD  18827  frlmsslsp  18829  frlmsslspOLD  18830  frlmup1  18832  frlmup2  18833  lindfind2  18853  lindfrn  18856  f1lindf  18857  islindf4  18873  mamudi  18905  mamudir  18906  1marepvmarrepid  19077  mdetrlin  19104  smadiadetglem1  19173  smadiadetg  19175  cramerimplem1  19185  mat2pmatscmxcl  19241  m2pmfzgsumcl  19249  pmatcollpw  19282  pmatcollpwfi  19283  pmatcollpw3fi1lem1  19287  cpmidpmatlem2  19372  cpmadugsumlemF  19377  chcoeffeqlem  19386  ntrin  19562  topssnei  19625  restbas  19659  restntr  19683  cnntri  19772  fiuncmp  19904  nllyrest  19987  nllyidm  19990  hausllycmp  19995  cldllycmp  19996  hauspwdom  20002  txcld  20104  txcn  20127  txlly  20137  txnlly  20138  txhaus  20148  txlm  20149  txkgen  20153  xkococnlem  20160  cnmpt2res  20178  xkoinjcn  20188  basqtop  20212  qtopeu  20217  trfbas2  20344  neifil  20381  hausflim  20482  alexsubALTlem2  20548  cnextfval  20562  cnextfvval  20565  cnextf  20566  clssubg  20607  utop2nei  20753  utop3cls  20754  utopreg  20755  psmetlecl  20819  xmetlecl  20849  prdsxmetlem  20871  bldisj  20901  imasf1obl  20991  prdsbl  20994  stdbdmet  21019  stdbdmopn  21021  met2ndci  21025  metcnp  21044  metusttoOLD  21060  metustto  21061  metustexhalfOLD  21066  metustexhalf  21067  cfilucfilOLD  21072  cfilucfil  21073  metucnOLD  21091  metucn  21092  lssnlm  21209  nmotri  21246  nmoid  21249  tgioo  21301  blcvx  21303  xrsmopn  21317  reperflem  21323  reconnlem2  21332  opnreen  21336  metdsge  21353  metdsre  21357  metdscnlem  21359  metnrmlem1a  21362  metnrmlem1  21363  metnrmlem3  21365  cncfmet  21412  cnmpt2pc  21428  icopnfcnv  21442  icopnfhmeo  21443  cnllycmp  21456  evth  21459  lebnumii  21466  nmoleub2lem3  21598  iscfil2  21705  cfil3i  21708  iscfil3  21712  cfilfcls  21713  iscau3  21717  iscmet3lem2  21731  caubl  21746  lmcau  21751  rrxcph  21824  minveclem2  21841  pjthlem1  21852  pjthlem2  21853  ivthicc  21870  ovollecl  21894  ovolunlem1a  21907  ovolunnul  21911  ovoliunlem1  21913  ismbl2  21938  nulmbl2  21947  unmbl  21948  volun  21955  voliunlem2  21961  ioombl1lem2  21969  uniioombllem2a  21991  uniioombllem3  21994  uniioombllem4  21995  dyaddisjlem  22004  dyadmaxlem  22006  opnmbllem  22010  volsup2  22014  volcn  22015  ismbfd  22047  mbfi1fseqlem1  22122  mbfi1fseqlem5  22126  itg2lecl  22145  itg2monolem2  22158  itg2gt0  22167  itgspliticc  22243  ellimc3  22283  limcres  22290  dvfval  22301  dvres3  22317  dvres3a  22318  dvnff  22326  dvnadd  22332  dvn2bss  22333  dvnres  22334  dvcmul  22347  dvcmulf  22348  dvmptres3  22359  dvmptres2  22365  dvmptntr  22374  dvexp3  22379  dvferm1lem  22385  dvlip  22394  dvlipcn  22395  dvlip2  22396  c1liplem1  22397  dvgt0lem1  22403  dvgt0lem2  22404  dvne0  22412  lhop1lem  22414  lhop2  22416  lhop  22417  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcvx  22421  dvfsumle  22422  dvfsumabs  22424  dvfsumlem2  22428  ftc1lem6  22442  ftc1  22443  ftc2ditglem  22446  itgsubstlem  22449  tdeglem4  22458  mdegaddle  22474  mdegmullem  22478  ply1rem  22564  fta1glem2  22567  fta1blem  22569  ig1peu  22572  ig1pdvds  22577  dgrmulc  22668  dgrcolem1  22670  plydivlem4  22692  plydiveu  22694  fta1lem  22703  vieta1lem1  22706  vieta1lem2  22707  plyexmo  22709  taylfvallem1  22752  taylfval  22754  tayl0  22757  taylplem1  22758  taylply2  22763  taylply  22764  dvtaylp  22765  dvntaylp  22766  dvntaylp0  22767  taylthlem1  22768  taylthlem2  22769  ulmcaulem  22789  ulmcau  22790  ulmcn  22794  ulmdvlem1  22795  radcnvlem1  22808  radcnvle  22815  psercn  22821  pserdvlem2  22823  pserdv  22824  abelth  22836  cosordlem  22918  tanregt0  22926  dvlog2lem  23033  efopn  23039  logtayllem  23040  logccv  23044  cxplt3  23081  cxpmul2zd  23097  cxpltd  23100  cxpled  23101  cxplt3d  23113  cxple3d  23114  dvsqrt  23118  cxpcn3  23122  cxpaddle  23126  cxpeq  23131  angcan  23134  angvald  23136  ang180lem2  23142  ang180  23146  isosctrlem3  23154  dquartlem1  23182  atantayl2  23269  leibpilem1  23271  leibpi  23273  log2tlbnd  23276  birthdaylem3  23283  xrlimcnp  23298  efrlim  23299  o1cxp  23304  jensenlem2  23317  jensen  23318  fsumharmonic  23341  wilthlem1  23342  basellem3  23356  basellem6  23359  basellem8  23361  ppisval  23377  chtwordi  23430  ppiwordi  23436  mumullem2  23454  dvdsmulf1o  23470  fsumvma  23488  fsumvma2  23489  chpchtsum  23494  chpub  23495  logfacubnd  23496  dchrmulcl  23524  dchrinv  23536  dchrptlem1  23539  dchrptlem2  23540  sumdchr2  23545  dchr2sum  23548  bposlem7  23565  lgslem1  23571  lgslem3  23573  lgsdirprm  23604  lgsqrlem2  23617  lgseisenlem1  23624  lgseisenlem2  23625  lgseisenlem4  23627  lgseisen  23628  lgsquadlem1  23629  lgsquad2lem1  23633  lgsquad3  23636  m1lgs  23637  2sqlem7  23645  chebbnd1lem2  23655  chebbnd1lem3  23656  rplogsumlem1  23669  rpvmasumlem  23672  dchrvmasumlem1  23680  dchrvmasum2lem  23681  dchrvmasumlema  23685  dchrisum0flblem2  23694  dchrisum0fno1  23696  dchrisum0re  23698  logdivsum  23718  pntrsumbnd2  23752  pntpbnd1a  23770  pntpbnd1  23771  pntibndlem2  23776  pntlemr  23787  pntlemj  23788  pntlemf  23790  pnt2  23798  padicabv  23815  ostth2lem2  23819  f1otrg  24174  brbtwn2  24208  colinearalglem2  24210  axcgrtr  24218  axcgrid  24219  axsegconlem7  24226  axsegcon  24230  ax5seglem3  24234  ax5seglem6  24237  ax5seg  24241  axpaschlem  24243  axlowdimlem17  24261  axcontlem2  24268  axcontlem4  24270  axcontlem7  24273  axcontlem8  24274  ecgrtg  24286  usgraidx2v  24393  iseupa  24965  eupap1  24976  eupath2lem3  24979  numclwwlkovf2ex  25086  nmobndi  25690  ubthlem2  25787  ubthlem3  25788  minvecolem2  25791  shuni  26218  pjhthlem1  26309  chscllem2  26556  pjcompi  26590  mayete3i  26646  mayete3iOLD  26647  unoplin  26839  hmoplin  26861  nmophmi  26950  mdslmd4i  27252  preqsnd  27418  isoun  27520  xrofsup  27582  eliccelico  27588  elicoelioo  27589  difioo  27593  rexdiv  27622  2sqmod  27636  xrge0addgt0  27681  omndadd2d  27698  omndadd2rd  27699  omndmul2  27702  ofldchr  27804  unitdivcld  27883  xrge0mulc1cn  27923  qqhnm  27971  esumcst  28071  esumfsup  28076  esumpmono  28085  esumcvg  28092  difelsiga  28133  1stmbfm  28231  2ndmbfm  28232  dya2icoseg  28248  sibfinima  28281  probmeasb  28369  orvcgteel  28406  orvclteel  28411  ballotlemsima  28454  ballotlemfrceq  28467  sgnmul  28481  ccatmulgnn0dir  28496  ofccat  28497  lgamucov  28580  lgamcvg2  28597  subfacp1lem2a  28624  subfaclim  28632  erdsze2lem2  28648  cvmliftlem2  28731  cvmliftlem10  28739  cvmliftlem13  28741  cvmliftiota  28746  cvmlift2lem9  28756  cvmlift2lem11  28758  cvmlift2lem12  28759  cvmliftphtlem  28762  cvmlift3lem6  28769  cvmlift3lem7  28770  cvmlift3lem9  28772  snmlff  28774  mrsubfval  28868  rprisefaccl  29145  trpredelss  29315  trpredpo  29318  wzel  29380  wsuclem  29381  nodenselem5  29445  nobndlem6  29457  brsegle  29758  fin2so  30040  opnmbllem0  30050  mblfinlem3  30053  mblfinlem4  30054  itg2addnclem  30066  itg2addnc  30069  itg2gt0cn  30070  ftc1cnnclem  30088  ftc1cnnc  30089  areacirclem5  30111  opnregcld  30148  indexdom  30225  sstotbnd2  30270  isbnd3  30280  isbnd3b  30281  cntotbnd  30292  ismtyima  30299  heibor1lem  30305  heiborlem8  30314  rrncmslem  30328  reheibor  30335  mzpsubst  30681  eldioph2lem1  30693  eldioph2lem2  30694  eldioph2b  30696  diophin  30706  irrapxlem2  30759  irrapxlem4  30761  irrapxlem5  30762  pellexlem1  30765  pellexlem2  30766  pellexlem6  30770  elpell1qr2  30808  pell1qrgaplem  30809  pell1qrgap  30810  pellqrex  30815  pellfundex  30822  pellfund14  30834  rmspecsqrtnq  30842  rmxyadd  30857  expmordi  30883  rmxypos  30885  jm2.24  30901  congsub  30908  mzpcong  30910  congrep  30911  acongtr  30916  acongrep  30918  jm2.19lem1  30931  jm2.22  30937  jm2.23  30938  jm2.26lem3  30943  jm2.26  30944  jm2.27a  30947  fnwe2lem2  30997  aomclem6  31005  hbtlem2  31073  hbtlem4  31075  hbtlem5  31077  dgraa0p  31098  rngunsnply  31122  acsfn1p  31148  proot1hash  31160  itgpowd  31182  expgrowth  31240  ioondisj2  31525  ioondisj1  31526  elicore  31537  eliocre  31547  ioossioobi  31557  lptioo2  31637  limcresiooub  31648  cncfuni  31689  cncfiooicclem1  31696  cxpcncf2  31703  dvcnre  31711  dvresntr  31713  dvmptresicc  31716  dvresioo  31718  dvbdfbdioolem1  31725  dvnmptdivc  31735  dvnxpaek  31739  itgsinexplem1  31752  itgcoscmulx  31768  itgiccshift  31779  itgperiod  31780  stoweidlem11  31793  stoweidlem26  31808  stoweidlem34  31816  stoweidlem36  31818  stoweidlem38  31820  stirlinglem5  31860  dirkercncflem2  31886  dirkercncflem4  31888  fourierdlem20  31909  fourierdlem58  31947  fourierdlem72  31961  fourierdlem73  31962  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem79  31968  fourierdlem80  31969  fourierdlem87  31976  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem107  31996  fourierdlem113  32002  sqwvfoura  32011  sqwvfourb  32012  fourierswlem  32013  fouriersw  32014  etransclem46  32063  etransclem47  32064  uhgeq12d  32375  usgedgvadf1  32415  usgedgvadf1ALT  32418  lkrlsp  34827  lshpkrlem5  34839  ldualssvscl  34883  ldualssvsubcl  34884  llnmlplnN  35263  llncvrlpln  35282  pmapjat1  35577  pclfinN  35624  lautlt  35815  lauteq  35819  lautco  35821  ltrn11  35850  ltrnle  35853  ltrneq2  35872  cdlemednuN  36025  cdleme20k  36045  cdleme20l2  36047  cdleme20l  36048  cdleme20m  36049  cdleme21c  36053  cdleme22e  36070  cdleme22eALTN  36071  cdlemefrs32fva  36126  cdlemg4g  36342  cdlemg18b  36405  cdlemg18c  36406  cdlemj3  36549  dia2dimlem5  36795  dvhopN  36843  cdlemm10N  36845  dihjatcclem4  37148  dochexmidlem2  37188  lclkrlem2o  37248  lcfrlem5  37273  lcfrlem6  37274  lcdlssvscl  37333  mapdpglem6  37405  mapdpglem9  37407  mapdpglem12  37410  mapdpglem14  37412  mapdindp0  37446  hdmaprnlem7N  37585  hdmaprnlem8N  37586  hdmaprnlem3eN  37588  hgmapvvlem3  37655
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
  Copyright terms: Public domain W3C validator