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

Theorem syl2anr 596
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 595 . 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 208  df-an 397
This theorem is referenced by:  swopo  5477  ordintdif  6233  funco  6388  resdif  6628  fvcofneq  6851  fnprb  6962  fntpb  6963  isotr  7078  weisoeq  7097  brrpssg  7440  findsg  7598  coexg  7623  xpexgALT  7671  fnsuppres  7846  wfrlem10  7953  oaass  8176  oeword  8205  oeworde  8208  mapsnd  8438  ixpssmapg  8480  pw2f1olem  8609  domsdomtr  8640  xpen  8668  mapen  8669  mapdom1  8670  mapfienlem1  8856  elfir  8867  wdomen2  9029  carden2b  9384  harcard  9395  isinffi  9409  acnlem  9462  acndom  9465  alephdom  9495  fin23lem21  9749  fin23lem39  9760  isf32lem5  9767  fin1a2lem12  9821  axdc3lem2  9861  ttukeylem1  9919  pwcfsdom  9993  canthp1  10064  nqereu  10339  addpqf  10354  axmulf  10556  axmulass  10567  axdistr  10568  ltaddnegr  10844  negeu  10864  fimaxre3  11575  nnsub  11669  nn0sub  11935  ltsubnn0  11936  elz2  11987  uzaddcl  12292  qaddcl  12352  xltneg  12598  xleneg  12599  supxrbnd1  12702  infxrgelb  12716  iccneg  12846  uzsubsubfz  12917  fzsplit2  12920  fzadd2  12930  fzss1  12934  uzsplit  12967  fz0fzdiffz0  13004  difelfzle  13008  difelfznle  13009  fvffz0  13013  preduz  13017  predfz  13020  fzonlt0  13048  fzouzsplit  13060  fzo0addelr  13080  eluzgtdifelfzo  13087  elfzodifsumelfzo  13091  ssfzo12  13118  elfznelfzob  13131  fllt  13164  flflp1  13165  uzsup  13219  negmod  13272  modifeq2int  13289  modfzo0difsn  13299  modsumfzodifsn  13300  om2uzlt2i  13307  nn0ennn  13335  suppssfz  13350  seqfveq2  13380  sermono  13390  seqf1o  13399  ser1const  13414  rpexpmord  13520  mulsubdivbinom2  13610  faclbnd  13638  bcval4  13655  bcpasc  13669  hashkf  13680  hashunx  13735  hashfacen  13800  fz1isolem  13807  ishashinf  13809  seqcoll  13810  ccatval1  13918  ccatval21sw  13927  ccatrn  13931  ccatalpha  13935  swrdnd0  14007  swrd0  14008  swrdfv2  14011  swrdspsleq  14015  addlenpfx  14041  ccatpfx  14051  swrdswrd  14055  pfxccatin12lem2  14081  pfxccat3  14084  swrdccat  14085  revccat  14116  repswswrd  14134  cshwmodn  14145  cshwidxmod  14153  repswcshw  14162  2cshwid  14164  2cshwcom  14166  2cshwcshw  14175  cshwcshid  14177  cshwcsh2id  14178  s1co  14183  cshco  14186  trclub  14346  shftfval  14417  seqshft  14432  crim  14462  caubnd  14706  limsuplt  14824  isercolllem2  15010  fsumcvg  15057  fsumcvg2  15072  fsumshftm  15124  fsumo1  15155  isumshft  15182  harmonic  15202  cvgrat  15227  mertenslem1  15228  zprod  15279  fprodmodd  15339  bpolylem  15390  bpolysum  15395  bpolydiflem  15396  fsumkthpow  15398  rpnnen2lem12  15566  dvdsval3  15599  negdvdsb  15614  dvdsnegb  15615  dvdsmul1  15619  dvdsabseq  15651  dvdsssfz1  15656  odd2np1  15678  divalglem8  15739  ndvdsadd  15749  dfgcd2  15882  dvdssqim  15892  nn0seqcvgd  15902  seq1st  15903  algcvgblem  15909  lcmf  15965  lcmfunsnlem2  15972  cncongr2  16000  prmdvdsfz  16037  isprm7  16040  prmndvdsfaclt  16055  powm2modprm  16128  modprm0  16130  modprmn0modprm0  16132  pythagtriplem1  16141  pythagtriplem4  16144  pythagtriplem8  16148  pythagtriplem9  16149  pythagtriplem12  16151  pythagtriplem14  16153  pythagtriplem16  16155  pcexp  16184  pc2dvds  16203  pcz  16205  fldivp1  16221  pcfac  16223  oddprmdvds  16227  pockthg  16230  infpnlem1  16234  prmreclem1  16240  prmreclem2  16241  1arith  16251  4sqlem11  16279  vdwlem2  16306  vdwlem8  16312  vdwnnlem2  16320  prmgaplem7  16381  prmgaplem8  16382  cshwshashlem2  16418  cshwshashlem3  16419  pwsval  16747  isacs1i  16916  funcsetcestrclem9  17401  ismgmid  17863  mhmpropd  17950  grpsubid1  18122  mulgnnp1  18174  mulgsubcl  18180  mulgnn0z  18192  mulgnndir  18194  mulgneg2  18199  lagsubg  18280  ghmco  18316  symg2bas  18455  symgextfv  18475  pgpfi2  18660  efgsfo  18794  frgpupf  18828  frgpup1  18830  gsummptshft  18985  telgsumfzslem  19037  telgsums  19042  ablfac1eu  19124  pgpfac1lem2  19126  ablfaclem3  19138  dvdsrid  19330  dvdsrneg  19333  dvr1  19368  abv1  19533  lmodfopne  19601  lbsexg  19865  gsummoncoe1  20400  xrsds  20516  znf1o  20626  lindfmm  20899  matecl  20962  mavmul0g  21090  gsummatr01  21196  mp2pm2mplem4  21345  chfacfisf  21390  chfacfisfcpmat  21391  chfacfpmmulgsum2  21401  cpmadugsumlemF  21412  isclo  21623  resttopon  21697  restcld  21708  restcls  21717  iscn  21771  iscnp  21773  cnco  21802  cndis  21827  cnindis  21828  cmpsub  21936  hauscmplem  21942  cmpfii  21945  ptcnplem  22157  txtube  22176  txcmplem1  22177  xkoptsub  22190  qtoptop  22236  kqfval  22259  hmeoco  22308  fileln0  22386  trfil1  22422  trfil2  22423  trufil  22446  elfm3  22486  hausflf2  22534  isucn  22814  bl2in  22937  metss2lem  23048  metss2  23049  stdbdxmet  23052  metrest  23061  nmfval2  23127  nmval2  23128  nmoix  23265  ioo2bl  23328  xrsxmet  23344  expcn  23407  elcncf  23424  icccvx  23481  cphsscph  23781  iscmet3  23823  causs  23828  metcld2  23837  metsscmetcld  23845  cncmet  23852  bcth3  23861  ovolgelb  24008  ovolfi  24022  shft2rab  24036  uniioombllem3  24113  dyadmax  24126  dyadmbl  24128  subopnmbl  24132  volcn  24134  mbfid  24163  mbfeqalem2  24170  mbfres  24172  cnmbf  24187  i1fmulc  24231  mbfi1fseqlem3  24245  mbfi1fseqlem4  24246  itg2seq  24270  itg2gt0  24288  itgss3  24342  dvexp  24477  plypow  24722  plyeq0lem  24727  coeidlem  24754  dgrlt  24783  dgrcolem2  24791  elqaalem2  24836  aacjcl  24843  aaliou3lem1  24858  aaliou3lem2  24859  pserdvlem2  24943  abelthlem8  24954  cosord  25043  sinord  25045  resinf1o  25047  relogexp  25106  logdivlt  25131  advlogexp  25165  logcxp  25179  cxpcl  25184  rpcxpcl  25186  cxpne0  25187  logbchbase  25276  logbgt0b  25298  birthdaylem2  25457  cxplim  25476  divsqrtsumo1  25488  zetacvg  25519  wilthlem1  25572  ftalem7  25583  basellem1  25585  issqf  25640  sqf11  25643  sgmf  25649  sgmnncl  25651  sqff1o  25686  dvdsflsumcom  25692  dvdsmulf1o  25698  sgmppw  25700  chtublem  25714  chtub  25715  logexprlim  25728  bposlem3  25789  bposlem5  25791  bposlem6  25792  lgsdirnn0  25847  gausslemma2dlem1a  25868  gausslemma2dlem5a  25873  lgsquad2  25889  lgsquad3  25890  2sqreulem1  25949  2sqreunnlem1  25952  dchrisumlem1  25992  dchrisumlem2  25993  dchrisumlem3  25994  mulogsumlem  26034  brbtwn  26612  uspgrupgrushgr  26889  usgrumgruspgr  26892  cusgrfilem2  27165  finsumvtxdg2ssteplem2  27255  crctcshwlkn0lem4  27518  crctcshwlkn0lem6  27520  crctcshwlkn0lem7  27521  crctcshwlkn0  27526  elwspths2spth  27673  rusgrnumwwlk  27681  clwlkclwwlklem2fv2  27701  erclwwlknref  27775  1to2vfriswmgr  27985  4cycl2v2nb  27995  frgr2wwlkeqm  28037  nvo00  28465  nmorepnf  28472  ubthlem1  28574  normpyc  28850  occon3  29001  pjpreeq  29102  idcnop  29685  riesz3i  29766  cnlnssadj  29784  rnbra  29811  strlem3a  29956  cvcon3  29988  ssdmd1  30017  ssdmd2  30018  relfi  30280  fzsplit3  30443  prmsimpcyc  30783  esumcst  31221  dmvlsiga  31287  ballotlemimin  31662  bnj545  32066  bnj929  32107  bnj953  32110  pthhashvtx  32271  derangsn  32314  iscvm  32403  cvmsval  32410  cvmliftlem7  32435  cvmlift2lem12  32458  mclsssvlem  32706  supfz  32857  faclimlem3  32874  noextenddif  33072  opnrebl2  33566  nn0prpwlem  33567  tailval  33618  nndivlub  33703  ctbssinf  34569  finixpnum  34758  ltflcei  34761  lindsdom  34767  lindsenlbs  34768  matunitlindflem2  34770  poimirlem4  34777  poimirlem14  34787  poimirlem15  34788  poimirlem19  34792  poimirlem20  34793  poimirlem22  34795  poimirlem24  34797  poimirlem28  34801  poimirlem30  34803  poimirlem31  34804  mblfinlem2  34811  mblfinlem3  34812  mblfinlem4  34813  ftc1anclem1  34848  ftc1anclem4  34851  ftc1anclem5  34852  ftc1anclem7  34854  ftc1anclem8  34855  ftc1anc  34856  caushft  34917  ismtyval  34959  heiborlem7  34976  heiborlem10  34979  heibor  34980  oexpreposd  39057  elrfirn  39170  ismrc  39176  nacsfix  39187  mzpcompact2lem  39226  eldiophb  39232  ellz1  39242  rexrabdioph  39269  congrep  39448  jm2.26a  39475  rngunsnply  39651  mendring  39670  iocmbl  39697  rp-isfinite5  39761  enrelmap  40221  expgrowthi  40542  cnfex  41162  xlimclim2lem  41996  climxlim2  42003  icccncfext  42046  itgsinexp  42116  iblspltprt  42134  itgspltprt  42140  fourierdlem50  42318  fourierswlem  42392  etransclem35  42431  zm1nn  43379  subsubelfzo0  43403  iccpartres  43455  iccelpart  43470  iccpartiun  43471  iccpartnel  43475  goldbachthlem1  43584  goldbachth  43586  odz2prm2pw  43602  2pwp1prm  43628  evenltle  43759  fpprwpprb  43782  sbgoldbaltlem2  43822  bgoldbachlt  43855  isomushgr  43868  isomuspgrlem1  43869  isomgrtr  43881  upgrwlkupwlk  43892  mgmhmpropd  43929  smndex1gid  44003  smndex1id  44011  2zrngamgm  44138  lincresunit3  44464  lincreslvec3  44465  isldepslvec2  44468  m1modmmod  44509  blengt1fldiv2p1  44581  dignn0flhalf  44606  nn0sumshdiglemA  44607  rrx2pnedifcoorneor  44631  aacllem  44830
  Copyright terms: Public domain W3C validator