MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl2anr Structured version   Visualization version   GIF version

Theorem syl2anr 494
Description: A double syllogism inference. For an implication-only version, see syl2imc 40. (Contributed by NM, 17-Sep-2013.)
Hypotheses
Ref Expression
syl2an.1 (𝜑𝜓)
syl2an.2 (𝜏𝜒)
syl2an.3 ((𝜓𝜒) → 𝜃)
Assertion
Ref Expression
syl2anr ((𝜏𝜑) → 𝜃)

Proof of Theorem syl2anr
StepHypRef Expression
1 syl2an.1 . . 3 (𝜑𝜓)
2 syl2an.2 . . 3 (𝜏𝜒)
3 syl2an.3 . . 3 ((𝜓𝜒) → 𝜃)
41, 2, 3syl2an 493 . 2 ((𝜑𝜏) → 𝜃)
54ancoms 468 1 ((𝜏𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 196  df-an 385
This theorem is referenced by:  swopo  4969  ordintdif  5691  funco  5842  resdif  6070  fvcofneq  6275  fnprb  6377  fntpb  6378  isotr  6486  weisoeq  6505  brrpssg  6837  findsg  6985  coexg  7010  xpexgALT  7052  fnsuppres  7209  wfrlem10  7311  oaass  7528  oeword  7557  oeworde  7560  ixpssmapg  7824  pw2f1olem  7949  domsdomtr  7980  xpen  8008  mapen  8009  mapdom1  8010  mapfienlem1  8193  elfir  8204  wdomen2  8365  carden2b  8676  harcard  8687  isinffi  8701  acnlem  8754  acndom  8757  alephdom  8787  fin23lem21  9044  fin23lem39  9055  isf32lem5  9062  fin1a2lem12  9116  axdc3lem2  9156  ttukeylem1  9214  pwcfsdom  9284  canthp1  9355  nqereu  9630  addpqf  9645  axmulf  9846  axmulass  9857  axdistr  9858  ltaddnegr  10131  negeu  10150  fimaxre3  10849  nnsub  10936  nn0sub  11220  ltsubnn0  11221  elz2  11271  uzaddcl  11620  qaddcl  11680  xltneg  11922  xleneg  11923  supxrbnd1  12023  infxrgelb  12037  iccneg  12164  uzsubsubfz  12234  fzsplit2  12237  fzadd2  12247  fzss1  12251  uzsplit  12281  fz0fzdiffz0  12317  difelfzle  12321  difelfznle  12322  fvffz0  12326  preduz  12330  predfz  12333  fzonlt0  12360  fzouzsplit  12372  fzo0addelr  12390  eluzgtdifelfzo  12397  elfzodifsumelfzo  12401  ssfzo12  12427  elfznelfzob  12440  fllt  12469  flflp1  12470  uzsup  12524  negmod  12577  modifeq2int  12594  modfzo0difsn  12604  modsumfzodifsn  12605  om2uzlt2i  12612  nn0ennn  12640  suppssfz  12656  seqfveq2  12685  sermono  12695  seqf1o  12704  ser1const  12719  mulsubdivbinom2  12908  faclbnd  12939  bcval4  12956  bcpasc  12970  hashkf  12981  hashunx  13036  hashfacen  13095  fz1isolem  13102  ishashinf  13104  seqcoll  13105  ccatalpha  13228  swrd0  13286  swrdfv2  13298  swrdspsleq  13301  swrdswrd  13312  swrdccatin12lem2  13340  swrdccat3  13343  revccat  13366  repswswrd  13382  cshwmodn  13392  cshwidxmod  13400  repswcshw  13409  2cshwid  13411  2cshwcom  13413  2cshwcshw  13422  cshwcshid  13424  cshwcsh2id  13425  s1co  13430  cshco  13433  trclub  13587  shftfval  13658  seqshft  13673  crim  13703  caubnd  13946  limsuplt  14058  isercolllem2  14244  fsumcvg  14290  fsumcvg2  14305  fsumshftm  14355  fsumo1  14385  isumshft  14410  harmonic  14430  cvgrat  14454  mertenslem1  14455  zprod  14506  fprodmodd  14567  bpolylem  14618  bpolysum  14623  bpolydiflem  14624  fsumkthpow  14626  rpnnen2lem12  14793  dvdsval3  14825  negdvdsb  14836  dvdsnegb  14837  dvdsmul1  14841  dvdsabseq  14873  dvdsssfz1  14878  odd2np1  14903  divalglem8  14961  ndvdsadd  14972  dfgcd2  15101  dvdssqim  15111  nn0seqcvgd  15121  seq1st  15122  algcvgblem  15128  lcmf  15184  lcmfunsnlem2  15191  cncongr2  15220  prmdvdsfz  15255  isprm7  15258  prmndvdsfaclt  15273  powm2modprm  15346  modprm0  15348  modprmn0modprm0  15350  pythagtriplem1  15359  pythagtriplem4  15362  pythagtriplem8  15366  pythagtriplem9  15367  pythagtriplem12  15369  pythagtriplem14  15371  pythagtriplem16  15373  pcexp  15402  pc2dvds  15421  pcz  15423  fldivp1  15439  pcfac  15441  oddprmdvds  15445  pockthg  15448  infpnlem1  15452  prmreclem1  15458  prmreclem2  15459  1arith  15469  4sqlem11  15497  vdwlem2  15524  vdwlem8  15530  vdwnnlem2  15538  prmgaplem7  15599  prmgaplem8  15600  cshwshashlem2  15641  cshwshashlem3  15642  pwsval  15969  isacs1i  16141  funcsetcestrclem9  16626  ismgmid  17087  mhmpropd  17164  grpsubid1  17323  mulgnnp1  17372  mulgsubcl  17378  mulgnn0z  17390  mulgnndir  17392  mulgnndirOLD  17393  mulgneg2  17398  lagsubg  17479  ghmco  17503  symg2bas  17641  symgextfv  17661  pgpfi2  17844  efgsfo  17975  frgpupf  18009  frgpup1  18011  gsummptshft  18159  telgsumfzslem  18208  telgsums  18213  ablfac1eu  18295  pgpfac1lem2  18297  ablfaclem3  18309  dvdsrid  18474  dvdsrneg  18477  dvr1  18512  abv1  18656  lmodfopne  18724  lbsexg  18985  gsummoncoe1  19495  xrsds  19608  znf1o  19719  lindfmm  19985  matecl  20050  mavmul0g  20178  gsummatr01  20284  mp2pm2mplem4  20433  chfacfisf  20478  chfacfisfcpmat  20479  chfacfpmmulgsum2  20489  cpmadugsumlemF  20500  isclo  20701  resttopon  20775  restcld  20786  restcls  20795  iscn  20849  iscnp  20851  cnco  20880  cndis  20905  cnindis  20906  cmpsub  21013  hauscmplem  21019  cmpfii  21022  ptcnplem  21234  txtube  21253  txcmplem1  21254  xkoptsub  21267  qtoptop  21313  kqfval  21336  hmeoco  21385  fileln0  21464  trfil1  21500  trfil2  21501  trufil  21524  elfm3  21564  hausflf2  21612  isucn  21892  bl2in  22015  metss2lem  22126  metss2  22127  stdbdxmet  22130  metrest  22139  nmfval2  22205  nmval2  22206  nmoix  22343  ioo2bl  22404  xrsxmet  22420  expcn  22483  elcncf  22500  icccvx  22557  iscmet3  22899  causs  22904  metcld2  22913  cmetss  22921  cncmet  22927  bcth3  22936  ovolgelb  23055  ovolfi  23069  shft2rab  23083  uniioombllem3  23159  dyadmax  23172  dyadmbl  23174  subopnmbl  23178  volcn  23180  mbfid  23209  mbfeqalem  23215  mbfres  23217  cnmbf  23232  i1fmulc  23276  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  itg2seq  23315  itg2gt0  23333  itgss3  23387  dvexp  23522  plypow  23765  plyeq0lem  23770  coeidlem  23797  dgrlt  23826  dgrcolem2  23834  elqaalem2  23879  aacjcl  23886  aaliou3lem1  23901  aaliou3lem2  23902  pserdvlem2  23986  abelthlem8  23997  cosord  24082  sinord  24084  resinf1o  24086  relogexp  24146  logdivlt  24171  advlogexp  24201  logcxp  24215  cxpcl  24220  rpcxpcl  24222  cxpne0  24223  logbchbase  24309  birthdaylem2  24479  cxplim  24498  divsqrtsumo1  24510  zetacvg  24541  wilthlem1  24594  ftalem7  24605  basellem1  24607  issqf  24662  sqf11  24665  sgmf  24671  sgmnncl  24673  sqff1o  24708  dvdsflsumcom  24714  dvdsmulf1o  24720  sgmppw  24722  chtublem  24736  chtub  24737  logexprlim  24750  bposlem3  24811  bposlem5  24813  bposlem6  24814  lgsdirnn0  24869  gausslemma2dlem1a  24890  gausslemma2dlem5a  24895  lgsquad2  24911  lgsquad3  24912  dchrisumlem1  24978  dchrisumlem2  24979  dchrisumlem3  24980  mulogsumlem  25020  brbtwn  25579  usgrafilem2  25941  cusgraexi  25997  cusgrafilem2  26008  usgra2wlkspthlem2  26148  vfwlkniswwlkn  26234  clwlkisclwwlklem2fv2  26311  hashnbgravdg  26440  nbhashuvtx1  26442  rusgranumwlk  26484  4cycl2v2nb  26543  frg2woteqm  26586  2spotmdisj  26595  extwwlkfablem1  26601  numclwwlk8  26642  nvo00  27000  nmorepnf  27007  ubthlem1  27110  normpyc  27387  occon3  27540  pjpreeq  27641  idcnop  28224  riesz3i  28305  cnlnssadj  28323  rnbra  28350  strlem3a  28495  cvcon3  28527  ssdmd1  28556  ssdmd2  28557  relfi  28797  fzsplit3  28940  esumcst  29452  dmvlsiga  29519  ballotlemimin  29894  bnj545  30219  bnj929  30260  bnj953  30263  derangsn  30406  iscvm  30495  cvmsval  30502  cvmliftlem7  30527  cvmlift2lem12  30550  mclsssvlem  30713  supfz  30866  faclimlem3  30884  nobndlem2  31092  opnrebl2  31486  nn0prpwlem  31487  tailval  31538  nndivlub  31627  finixpnum  32564  ltflcei  32567  lindsdom  32573  lindsenlbs  32574  matunitlindflem2  32576  poimirlem4  32583  poimirlem14  32593  poimirlem15  32594  poimirlem19  32598  poimirlem20  32599  poimirlem22  32601  poimirlem24  32603  poimirlem28  32607  poimirlem30  32609  poimirlem31  32610  mblfinlem2  32617  mblfinlem3  32618  mblfinlem4  32619  ftc1anclem1  32655  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  caushft  32727  ismtyval  32769  heiborlem7  32786  heiborlem10  32789  heibor  32790  elrfirn  36276  ismrc  36282  nacsfix  36293  mzpcompact2lem  36332  eldiophb  36338  ellz1  36348  rexrabdioph  36376  rpexpmord  36531  congrep  36558  jm2.26a  36585  rngunsnply  36762  mendring  36781  iocmbl  36817  rp-isfinite5  36882  enrelmap  37311  expgrowthi  37554  cnfex  38210  icccncfext  38773  itgsinexp  38846  iblspltprt  38865  itgspltprt  38871  fourierdlem50  39049  fourierswlem  39123  etransclem35  39162  iccpartres  39956  iccelpart  39971  iccpartiun  39972  iccpartnel  39976  goldbachthlem1  39995  goldbachth  39997  odz2prm2pw  40013  fmtnoprmfac1lem  40014  2pwp1prm  40041  sgoldbaltlem2  40202  bgoldbachlt  40227  bgoldbachltOLD  40234  addlenpfx  40261  pfxccatin12lem2  40287  pfxccat3  40289  zm1nn  40348  subsubelfzo0  40359  uspgrupgrushgr  40407  usgrumgruspgr  40410  cusgrfilem2  40672  upgr1wlkwlk  40847  crctcsh1wlkn0lem4  41016  crctcsh1wlkn0lem6  41018  crctcsh1wlkn0lem7  41019  crctcsh1wlkn0  41024  elwspths2spth  41171  rusgrnumwwlk  41178  clwlkclwwlklem2fv2  41205  is01wlk  41285  is0Trl  41291  1to2vfriswmgr  41449  4cycl2v2nb-av  41459  frgr2wwlkeqm  41496  av-numclwwlk8  41546  mgmhmpropd  41575  2zrngamgm  41729  lincresunit3  42064  lincreslvec3  42065  isldepslvec2  42068  m1modmmod  42110  blengt1fldiv2p1  42185  dignn0flhalf  42210  nn0sumshdiglemA  42211  aacllem  42356
  Copyright terms: Public domain W3C validator