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

Theorem syl2anr 597
Description: A double syllogism inference. For an implication-only version, see syl2imc 41. (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 596 . 2 ((𝜑𝜏) → 𝜃)
54ancoms 459 1 ((𝜏𝜑) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 206  df-an 397
This theorem is referenced by:  swopo  5554  ordintdif  6365  funco  6538  resdif  6802  fvcofneq  7039  fnprb  7154  fntpb  7155  isotr  7277  weisoeq  7296  brrpssg  7654  findsg  7828  coexg  7858  xpexgALT  7906  fnsuppres  8114  wfrlem10OLD  8256  oaass  8500  oeword  8529  oeworde  8532  mapsnd  8782  ixpssmapg  8824  enrefnn  8949  pw2f1olem  8978  domsdomtr  9014  xpen  9042  mapen  9043  mapdom1  9044  phplem2  9110  mapfienlem1  9299  elfir  9309  wdomen2  9471  carden2b  9861  harcard  9872  isinffi  9886  acnlem  9942  acndom  9945  alephdom  9975  fin23lem21  10233  fin23lem39  10244  isf32lem5  10251  fin1a2lem12  10305  axdc3lem2  10345  ttukeylem1  10403  pwcfsdom  10477  canthp1  10548  nqereu  10823  addpqf  10838  axmulf  11040  axmulass  11051  axdistr  11052  ltaddnegr  11329  negeu  11349  fimaxre3  12059  nnsub  12155  nn0sub  12421  ltsubnn0  12422  elz2  12475  uzaddcl  12783  qaddcl  12844  xltneg  13090  xleneg  13091  supxrbnd1  13194  infxrgelb  13208  iccneg  13343  uzsubsubfz  13417  fzsplit2  13420  fzadd2  13430  fzss1  13434  uzsplit  13467  fz0fzdiffz0  13504  difelfzle  13508  difelfznle  13509  fvffz0  13513  preduz  13517  predfz  13520  fzonlt0  13549  fzouzsplit  13561  fzo0addelr  13581  eluzgtdifelfzo  13588  elfzodifsumelfzo  13592  ssfzo12  13619  elfznelfzob  13632  fllt  13665  flflp1  13666  uzsup  13722  negmod  13775  modifeq2int  13792  modfzo0difsn  13802  modsumfzodifsn  13803  om2uzlt2i  13810  nn0ennn  13838  suppssfz  13853  seqfveq2  13884  sermono  13894  seqf1o  13903  ser1const  13918  rpexpmord  14027  mulsubdivbinom2  14116  faclbnd  14144  bcval4  14161  bcpasc  14175  hashkf  14186  hashunx  14240  hashfacenOLD  14306  fz1isolem  14314  ishashinf  14316  seqcoll  14317  ccatval1  14419  ccatval21sw  14427  ccatrn  14431  ccatalpha  14435  swrdnd0  14499  swrd0  14500  swrdfv2  14503  swrdspsleq  14507  addlenpfx  14533  ccatpfx  14543  swrdswrd  14547  pfxccatin12lem2  14573  pfxccat3  14576  swrdccat  14577  revccat  14608  repswswrd  14626  cshwmodn  14637  cshwidxmod  14645  repswcshw  14654  2cshwid  14656  2cshwcom  14658  2cshwcshw  14668  cshwcshid  14670  cshwcsh2id  14671  s1co  14676  cshco  14679  trclub  14837  shftfval  14909  seqshft  14924  crim  14954  caubnd  15197  limsuplt  15315  isercolllem2  15504  fsumcvg  15551  fsumcvg2  15566  fsumshftm  15620  fsumo1  15651  isumshft  15678  harmonic  15698  cvgrat  15722  mertenslem1  15723  zprod  15774  fprodmodd  15834  bpolylem  15885  bpolysum  15890  bpolydiflem  15891  fsumkthpow  15893  rpnnen2lem12  16061  dvdsval3  16094  negdvdsb  16109  dvdsnegb  16110  dvdsmul1  16114  dvdsabseq  16149  dvdsssfz1  16154  odd2np1  16177  divalglem8  16236  ndvdsadd  16246  dfgcd2  16381  dvdssqim  16389  nn0seqcvgd  16400  seq1st  16401  algcvgblem  16407  lcmf  16463  lcmfunsnlem2  16470  cncongr2  16498  prmdvdsfz  16535  isprm7  16538  prmndvdsfaclt  16555  powm2modprm  16629  modprm0  16631  modprmn0modprm0  16633  pythagtriplem1  16642  pythagtriplem4  16645  pythagtriplem8  16649  pythagtriplem9  16650  pythagtriplem12  16652  pythagtriplem14  16654  pythagtriplem16  16656  pcexp  16685  pc2dvds  16705  pcz  16707  fldivp1  16723  pcfac  16725  oddprmdvds  16729  pockthg  16732  infpnlem1  16736  prmreclem1  16742  prmreclem2  16743  1arith  16753  4sqlem11  16781  vdwlem2  16808  vdwlem8  16814  vdwnnlem2  16822  prmgaplem7  16883  prmgaplem8  16884  cshwshashlem2  16923  cshwshashlem3  16924  pwsval  17322  isacs1i  17491  funcsetcestrclem9  18005  ismgmid  18474  mhmpropd  18562  smndex1gid  18667  smndex1id  18675  grpsubid1  18785  mulgnnp1  18837  mulgsubcl  18843  mulgnn0z  18856  mulgnndir  18858  mulgneg2  18863  lagsubg  18945  ghmco  18981  symg2bas  19127  symgextfv  19153  pgpfi2  19341  efgsfo  19474  frgpupf  19508  frgpup1  19510  gsummptshft  19666  telgsumfzslem  19718  telgsums  19723  ablfac1eu  19805  pgpfac1lem2  19807  ablfaclem3  19819  dvdsrid  20027  dvdsrneg  20030  dvr1  20065  abv1  20239  lmodfopne  20307  lbsexg  20572  xrsds  20787  znf1o  20905  lindfmm  21180  gsummoncoe1  21621  matecl  21720  mavmul0g  21848  gsummatr01  21954  mp2pm2mplem4  22104  chfacfisf  22149  chfacfisfcpmat  22150  chfacfpmmulgsum2  22160  cpmadugsumlemF  22171  isclo  22384  resttopon  22458  restcld  22469  restcls  22478  iscn  22532  iscnp  22534  cnco  22563  cndis  22588  cnindis  22589  cmpsub  22697  hauscmplem  22703  cmpfii  22706  ptcnplem  22918  txtube  22937  txcmplem1  22938  xkoptsub  22951  qtoptop  22997  kqfval  23020  hmeoco  23069  fileln0  23147  trfil1  23183  trfil2  23184  trufil  23207  elfm3  23247  hausflf2  23295  isucn  23576  bl2in  23699  metss2lem  23813  metss2  23814  stdbdxmet  23817  metrest  23826  nmval2  23894  nmoix  24039  ioo2bl  24102  xrsxmet  24118  expcn  24181  elcncf  24198  icccvx  24259  cphsscph  24561  iscmet3  24603  causs  24608  metcld2  24617  metsscmetcld  24625  cncmet  24632  bcth3  24641  ovolgelb  24790  ovolfi  24804  shft2rab  24818  uniioombllem3  24895  dyadmax  24908  dyadmbl  24910  subopnmbl  24914  volcn  24916  mbfid  24945  mbfeqalem2  24952  mbfres  24954  cnmbf  24969  i1fmulc  25014  mbfi1fseqlem3  25028  mbfi1fseqlem4  25029  itg2seq  25053  itg2gt0  25071  itgss3  25125  dvexp  25263  plypow  25512  plyeq0lem  25517  coeidlem  25544  dgrlt  25573  dgrcolem2  25581  elqaalem2  25626  aacjcl  25633  aaliou3lem1  25648  aaliou3lem2  25649  pserdvlem2  25733  abelthlem8  25744  cosord  25833  sinord  25836  resinf1o  25838  relogexp  25897  logdivlt  25922  advlogexp  25956  logcxp  25970  cxpcl  25975  rpcxpcl  25977  cxpne0  25978  logbchbase  26067  logbgt0b  26089  birthdaylem2  26248  cxplim  26267  divsqrtsumo1  26279  zetacvg  26310  wilthlem1  26363  ftalem7  26374  basellem1  26376  issqf  26431  sqf11  26434  sgmf  26440  sgmnncl  26442  sqff1o  26477  dvdsflsumcom  26483  dvdsmulf1o  26489  sgmppw  26491  chtublem  26505  chtub  26506  logexprlim  26519  bposlem3  26580  bposlem5  26582  bposlem6  26583  lgsdirnn0  26638  gausslemma2dlem1a  26659  gausslemma2dlem5a  26664  lgsquad2  26680  lgsquad3  26681  2sqreulem1  26740  2sqreunnlem1  26743  dchrisumlem1  26783  dchrisumlem2  26784  dchrisumlem3  26785  mulogsumlem  26825  noextenddif  26962  brbtwn  27693  uspgrupgrushgr  27973  usgrumgruspgr  27976  cusgrfilem2  28249  finsumvtxdg2ssteplem2  28339  crctcshwlkn0lem4  28603  crctcshwlkn0lem6  28605  crctcshwlkn0lem7  28606  crctcshwlkn0  28611  elwspths2spth  28757  rusgrnumwwlk  28765  clwlkclwwlklem2fv2  28785  erclwwlknref  28858  1to2vfriswmgr  29068  4cycl2v2nb  29078  frgr2wwlkeqm  29120  nvo00  29548  nmorepnf  29555  ubthlem1  29657  normpyc  29933  occon3  30084  pjpreeq  30185  idcnop  30768  riesz3i  30849  cnlnssadj  30867  rnbra  30894  strlem3a  31039  cvcon3  31071  ssdmd1  31100  ssdmd2  31101  relfi  31365  fzsplit3  31539  prmsimpcyc  31905  esumcst  32490  dmvlsiga  32556  ballotlemimin  32933  bnj545  33335  bnj929  33376  bnj953  33379  pthhashvtx  33549  derangsn  33592  iscvm  33681  cvmsval  33688  cvmliftlem7  33713  cvmlift2lem12  33736  mclsssvlem  33984  supfz  34133  faclimlem3  34150  addsid1  34273  sltneg  34331  sleneg  34332  opnrebl2  34725  nn0prpwlem  34726  tailval  34777  nndivlub  34862  ctbssinf  35809  finixpnum  35995  ltflcei  35998  lindsdom  36004  lindsenlbs  36005  matunitlindflem2  36007  poimirlem4  36014  poimirlem14  36024  poimirlem15  36025  poimirlem19  36029  poimirlem20  36030  poimirlem22  36032  poimirlem24  36034  poimirlem28  36038  poimirlem30  36040  poimirlem31  36041  mblfinlem2  36048  mblfinlem3  36049  mblfinlem4  36050  ftc1anclem1  36083  ftc1anclem4  36086  ftc1anclem5  36087  ftc1anclem7  36089  ftc1anclem8  36090  ftc1anc  36091  caushft  36152  ismtyval  36191  heiborlem7  36208  heiborlem10  36211  heibor  36212  lcmineqlem8  40425  oexpreposd  40710  elrfirn  40921  ismrc  40927  nacsfix  40938  mzpcompact2lem  40977  eldiophb  40983  ellz1  40993  rexrabdioph  41020  congrep  41200  jm2.26a  41227  rngunsnply  41403  mendring  41422  iocmbl  41450  oeord2lim  41545  cantnfresb  41559  omabs2  41566  ofoafg  41569  dfno2  41605  rp-isfinite5  41694  enrelmap  42174  expgrowthi  42518  cnfex  43138  xlimclim2lem  43975  climxlim2  43982  icccncfext  44023  itgsinexp  44091  iblspltprt  44109  itgspltprt  44115  fourierdlem50  44292  fourierswlem  44366  etransclem35  44405  zm1nn  45429  subsubelfzo0  45453  iccpartres  45505  iccelpart  45520  iccpartiun  45521  iccpartnel  45525  goldbachthlem1  45632  goldbachth  45634  odz2prm2pw  45650  2pwp1prm  45676  evenltle  45804  fpprwpprb  45827  sbgoldbaltlem2  45867  bgoldbachlt  45900  isomushgr  45913  isomuspgrlem1  45914  isomgrtr  45926  upgrwlkupwlk  45937  mgmhmpropd  45974  2zrngamgm  46132  lincresunit3  46457  lincreslvec3  46458  isldepslvec2  46461  m1modmmod  46502  blengt1fldiv2p1  46574  dignn0flhalf  46599  nn0sumshdiglemA  46600  rrx2pnedifcoorneor  46697  aacllem  47143
  Copyright terms: Public domain W3C validator