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 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 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 197  df-an 385
This theorem is referenced by:  swopo  5074  ordintdif  5812  funco  5966  resdif  6195  fvcofneq  6407  fnprb  6513  fntpb  6514  isotr  6626  weisoeq  6645  brrpssg  6981  findsg  7135  coexg  7159  xpexgALT  7203  fnsuppres  7367  wfrlem10  7469  oaass  7686  oeword  7715  oeworde  7718  ixpssmapg  7980  pw2f1olem  8105  domsdomtr  8136  xpen  8164  mapen  8165  mapdom1  8166  mapfienlem1  8351  elfir  8362  wdomen2  8523  carden2b  8831  harcard  8842  isinffi  8856  acnlem  8909  acndom  8912  alephdom  8942  fin23lem21  9199  fin23lem39  9210  isf32lem5  9217  fin1a2lem12  9271  axdc3lem2  9311  ttukeylem1  9369  pwcfsdom  9443  canthp1  9514  nqereu  9789  addpqf  9804  axmulf  10005  axmulass  10016  axdistr  10017  ltaddnegr  10290  negeu  10309  fimaxre3  11008  nnsub  11097  nn0sub  11381  ltsubnn0  11382  elz2  11432  uzaddcl  11782  qaddcl  11842  xltneg  12086  xleneg  12087  supxrbnd1  12189  infxrgelb  12203  iccneg  12331  uzsubsubfz  12401  fzsplit2  12404  fzadd2  12414  fzss1  12418  uzsplit  12450  fz0fzdiffz0  12487  difelfzle  12491  difelfznle  12492  fvffz0  12496  preduz  12500  predfz  12503  fzonlt0  12530  fzouzsplit  12542  fzo0addelr  12562  eluzgtdifelfzo  12569  elfzodifsumelfzo  12573  ssfzo12  12601  elfznelfzob  12614  fllt  12647  flflp1  12648  uzsup  12702  negmod  12755  modifeq2int  12772  modfzo0difsn  12782  modsumfzodifsn  12783  om2uzlt2i  12790  nn0ennn  12818  suppssfz  12834  seqfveq2  12863  sermono  12873  seqf1o  12882  ser1const  12897  mulsubdivbinom2  13086  faclbnd  13117  bcval4  13134  bcpasc  13148  hashkf  13159  hashunx  13213  hashfacen  13276  fz1isolem  13283  ishashinf  13285  seqcoll  13286  ccatval21sw  13403  ccatalpha  13411  swrd0  13480  swrdfv2  13492  swrdspsleq  13495  swrdswrd  13506  swrdccatin12lem2  13535  swrdccat3  13538  revccat  13561  repswswrd  13577  cshwmodn  13587  cshwidxmod  13595  repswcshw  13604  2cshwid  13606  2cshwcom  13608  2cshwcshw  13617  cshwcshid  13619  cshwcsh2id  13620  s1co  13625  cshco  13628  trclub  13783  shftfval  13854  seqshft  13869  crim  13899  caubnd  14142  limsuplt  14254  isercolllem2  14440  fsumcvg  14487  fsumcvg2  14502  fsumshftm  14557  fsumo1  14588  isumshft  14615  harmonic  14635  cvgrat  14659  mertenslem1  14660  zprod  14711  fprodmodd  14772  bpolylem  14823  bpolysum  14828  bpolydiflem  14829  fsumkthpow  14831  rpnnen2lem12  14998  dvdsval3  15031  negdvdsb  15045  dvdsnegb  15046  dvdsmul1  15050  dvdsabseq  15082  dvdsssfz1  15087  odd2np1  15112  divalglem8  15170  ndvdsadd  15181  dfgcd2  15310  dvdssqim  15320  nn0seqcvgd  15330  seq1st  15331  algcvgblem  15337  lcmf  15393  lcmfunsnlem2  15400  cncongr2  15429  prmdvdsfz  15464  isprm7  15467  prmndvdsfaclt  15482  powm2modprm  15555  modprm0  15557  modprmn0modprm0  15559  pythagtriplem1  15568  pythagtriplem4  15571  pythagtriplem8  15575  pythagtriplem9  15576  pythagtriplem12  15578  pythagtriplem14  15580  pythagtriplem16  15582  pcexp  15611  pc2dvds  15630  pcz  15632  fldivp1  15648  pcfac  15650  oddprmdvds  15654  pockthg  15657  infpnlem1  15661  prmreclem1  15667  prmreclem2  15668  1arith  15678  4sqlem11  15706  vdwlem2  15733  vdwlem8  15739  vdwnnlem2  15747  prmgaplem7  15808  prmgaplem8  15809  cshwshashlem2  15850  cshwshashlem3  15851  pwsval  16193  isacs1i  16365  funcsetcestrclem9  16850  ismgmid  17311  mhmpropd  17388  grpsubid1  17547  mulgnnp1  17596  mulgsubcl  17602  mulgnn0z  17614  mulgnndir  17616  mulgnndirOLD  17617  mulgneg2  17622  lagsubg  17703  ghmco  17727  symg2bas  17864  symgextfv  17884  pgpfi2  18067  efgsfo  18198  frgpupf  18232  frgpup1  18234  gsummptshft  18382  telgsumfzslem  18431  telgsums  18436  ablfac1eu  18518  pgpfac1lem2  18520  ablfaclem3  18532  dvdsrid  18697  dvdsrneg  18700  dvr1  18735  abv1  18881  lmodfopne  18949  lbsexg  19212  gsummoncoe1  19722  xrsds  19837  znf1o  19948  lindfmm  20214  matecl  20279  mavmul0g  20407  gsummatr01  20513  mp2pm2mplem4  20662  chfacfisf  20707  chfacfisfcpmat  20708  chfacfpmmulgsum2  20718  cpmadugsumlemF  20729  isclo  20939  resttopon  21013  restcld  21024  restcls  21033  iscn  21087  iscnp  21089  cnco  21118  cndis  21143  cnindis  21144  cmpsub  21251  hauscmplem  21257  cmpfii  21260  ptcnplem  21472  txtube  21491  txcmplem1  21492  xkoptsub  21505  qtoptop  21551  kqfval  21574  hmeoco  21623  fileln0  21701  trfil1  21737  trfil2  21738  trufil  21761  elfm3  21801  hausflf2  21849  isucn  22129  bl2in  22252  metss2lem  22363  metss2  22364  stdbdxmet  22367  metrest  22376  nmfval2  22442  nmval2  22443  nmoix  22580  ioo2bl  22643  xrsxmet  22659  expcn  22722  elcncf  22739  icccvx  22796  iscmet3  23137  causs  23142  metcld2  23151  cmetss  23159  cncmet  23165  bcth3  23174  ovolgelb  23294  ovolfi  23308  shft2rab  23322  uniioombllem3  23399  dyadmax  23412  dyadmbl  23414  subopnmbl  23418  volcn  23420  mbfid  23448  mbfeqalem  23454  mbfres  23456  cnmbf  23471  i1fmulc  23515  mbfi1fseqlem3  23529  mbfi1fseqlem4  23530  itg2seq  23554  itg2gt0  23572  itgss3  23626  dvexp  23761  plypow  24006  plyeq0lem  24011  coeidlem  24038  dgrlt  24067  dgrcolem2  24075  elqaalem2  24120  aacjcl  24127  aaliou3lem1  24142  aaliou3lem2  24143  pserdvlem2  24227  abelthlem8  24238  cosord  24323  sinord  24325  resinf1o  24327  relogexp  24387  logdivlt  24412  advlogexp  24446  logcxp  24460  cxpcl  24465  rpcxpcl  24467  cxpne0  24468  logbchbase  24554  birthdaylem2  24724  cxplim  24743  divsqrtsumo1  24755  zetacvg  24786  wilthlem1  24839  ftalem7  24850  basellem1  24852  issqf  24907  sqf11  24910  sgmf  24916  sgmnncl  24918  sqff1o  24953  dvdsflsumcom  24959  dvdsmulf1o  24965  sgmppw  24967  chtublem  24981  chtub  24982  logexprlim  24995  bposlem3  25056  bposlem5  25058  bposlem6  25059  lgsdirnn0  25114  gausslemma2dlem1a  25135  gausslemma2dlem5a  25140  lgsquad2  25156  lgsquad3  25157  dchrisumlem1  25223  dchrisumlem2  25224  dchrisumlem3  25225  mulogsumlem  25265  brbtwn  25824  uspgrupgrushgr  26117  usgrumgruspgr  26120  cusgrfilem2  26408  finsumvtxdg2ssteplem2  26498  crctcshwlkn0lem4  26761  crctcshwlkn0lem6  26763  crctcshwlkn0lem7  26764  crctcshwlkn0  26769  elwspths2spth  26934  rusgrnumwwlk  26942  clwlkclwwlklem2fv2  26962  erclwwlknref  27033  clwwlknonex2e  27085  1to2vfriswmgr  27259  4cycl2v2nb  27269  frgr2wwlkeqm  27311  clwwlkccatlem  27331  nvo00  27744  nmorepnf  27751  ubthlem1  27854  normpyc  28131  occon3  28284  pjpreeq  28385  idcnop  28968  riesz3i  29049  cnlnssadj  29067  rnbra  29094  strlem3a  29239  cvcon3  29271  ssdmd1  29300  ssdmd2  29301  relfi  29541  fzsplit3  29681  esumcst  30253  dmvlsiga  30320  ballotlemimin  30695  bnj545  31091  bnj929  31132  bnj953  31135  derangsn  31278  iscvm  31367  cvmsval  31374  cvmliftlem7  31399  cvmlift2lem12  31422  mclsssvlem  31585  supfz  31739  faclimlem3  31757  noextenddif  31946  opnrebl2  32441  nn0prpwlem  32442  tailval  32493  nndivlub  32582  finixpnum  33524  ltflcei  33527  lindsdom  33533  lindsenlbs  33534  matunitlindflem2  33536  poimirlem4  33543  poimirlem14  33553  poimirlem15  33554  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem24  33563  poimirlem28  33567  poimirlem30  33569  poimirlem31  33570  mblfinlem2  33577  mblfinlem3  33578  mblfinlem4  33579  ftc1anclem1  33615  ftc1anclem4  33618  ftc1anclem5  33619  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  caushft  33687  ismtyval  33729  heiborlem7  33746  heiborlem10  33749  heibor  33750  elrfirn  37575  ismrc  37581  nacsfix  37592  mzpcompact2lem  37631  eldiophb  37637  ellz1  37647  rexrabdioph  37675  rpexpmord  37830  congrep  37857  jm2.26a  37884  rngunsnply  38060  mendring  38079  iocmbl  38115  rp-isfinite5  38180  enrelmap  38608  expgrowthi  38849  cnfex  39501  xlimclim2lem  40383  climxlim2  40390  icccncfext  40418  itgsinexp  40488  iblspltprt  40507  itgspltprt  40513  fourierdlem50  40691  fourierswlem  40765  etransclem35  40804  zm1nn  41641  subsubelfzo0  41661  iccpartres  41679  iccelpart  41694  iccpartiun  41695  iccpartnel  41699  addlenpfx  41723  pfxccatin12lem2  41749  pfxccat3  41751  goldbachthlem1  41782  goldbachth  41784  odz2prm2pw  41800  2pwp1prm  41828  evenltle  41951  sbgoldbaltlem2  41993  bgoldbachlt  42026  bgoldbachltOLD  42032  upgrwlkupwlk  42046  mgmhmpropd  42110  2zrngamgm  42264  lincresunit3  42595  lincreslvec3  42596  isldepslvec2  42599  m1modmmod  42641  blengt1fldiv2p1  42712  dignn0flhalf  42737  nn0sumshdiglemA  42738  aacllem  42875
  Copyright terms: Public domain W3C validator