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

Theorem syl2anr 464
Description: A double syllogism inference. (Contributed by NM, 17-Sep-2013.)
Hypotheses
Ref Expression
syl2an.1  |-  ( ph  ->  ps )
syl2an.2  |-  ( ta 
->  ch )
syl2an.3  |-  ( ( ps  /\  ch )  ->  th )
Assertion
Ref Expression
syl2anr  |-  ( ( ta  /\  ph )  ->  th )

Proof of Theorem syl2anr
StepHypRef Expression
1 syl2an.1 . . 3  |-  ( ph  ->  ps )
2 syl2an.2 . . 3  |-  ( ta 
->  ch )
3 syl2an.3 . . 3  |-  ( ( ps  /\  ch )  ->  th )
41, 2, 3syl2an 463 . 2  |-  ( (
ph  /\  ta )  ->  th )
54ancoms 439 1  |-  ( ( ta  /\  ph )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem is referenced by:  swopo  4340  findsg  4699  coexg  5231  funco  5308  resdif  5510  fnsuppres  5748  isotr  5849  weisoeq  5869  xpexgALT  6086  brrpssg  6295  oaass  6575  oeword  6604  oeworde  6607  ixpssmapg  6862  pw2f1olem  6982  domsdomtr  7012  xpen  7040  mapen  7041  mapdom1  7042  elfir  7185  wdomen2  7307  carden2b  7616  harcard  7627  isinffi  7641  acnlem  7691  acndom  7694  alephdom  7724  fin23lem21  7981  fin23lem39  7992  isf32lem5  7999  fin1a2lem12  8053  ttukeylem1  8152  pwcfsdom  8221  canthp1  8292  nqereu  8569  addpqf  8584  axmulf  8784  axmulass  8795  axdistr  8796  negeu  9058  fimaxre3  9719  nnsub  9800  nn0sub  10030  elz2  10056  uzaddcl  10291  qaddcl  10348  xltneg  10560  xleneg  10561  supxrbnd1  10656  infmxrgelb  10669  iccneg  10773  fzsplit2  10831  fzss1  10846  uzsplit  10871  fzm1  10878  fzouzsplit  10917  fllt  10954  uzsup  10983  om2uzlt2i  11030  nn0ennn  11057  seqfveq2  11084  sermono  11094  seqf1o  11103  ser1const  11118  faclbnd  11319  bcval4  11336  bcpasc  11349  hashkf  11355  hashfacen  11408  fz1isolem  11415  seqcoll  11417  revccat  11500  s1co  11504  shftfval  11581  seqshft  11596  crim  11616  caubnd  11858  isercolllem2  12155  fsumcvg  12201  zsum  12207  fsumcvg2  12216  fsumshftm  12259  fsumo1  12286  isumshft  12314  harmonic  12333  cvgrat  12355  mertenslem1  12356  rpnnen2  12520  dvdsval3  12551  negdvdsb  12561  dvdsnegb  12562  dvdsmul1  12566  odd2np1  12603  divalglem8  12615  ndvdsadd  12623  dvdssqim  12748  nn0seqcvgd  12756  seq1st  12757  algcvgblem  12763  pythagtriplem1  12885  pythagtriplem4  12888  pythagtriplem8  12892  pythagtriplem9  12893  pythagtriplem12  12895  pythagtriplem14  12897  pythagtriplem16  12899  pcexp  12928  pc2dvds  12947  pcz  12949  fldivp1  12961  pcfac  12963  pockthg  12969  infpnlem1  12973  prmreclem1  12979  prmreclem2  12980  1arith  12990  4sqlem11  13018  vdwlem2  13045  vdwlem8  13051  vdwnnlem2  13059  pwsval  13401  isacs1i  13575  ismgmid  14403  mhmpropd  14437  grpsubid1  14567  mulgnnp1  14591  mulgsubcl  14597  mulgnn0z  14603  mulgnndir  14605  mulgneg2  14610  lagsubg  14695  ghmco  14718  pgpfi2  14933  efgsfo  15064  frgpup1  15100  ablfac1eu  15324  pgpfac1lem2  15326  ablfaclem3  15338  dvdsrid  15449  dvdsrneg  15452  dvr1  15487  abv1  15614  lbsexg  15933  xrsds  16430  znf1o  16521  isclo  16840  resttopon  16908  restcld  16919  restcls  16927  iscn  16981  iscnp  16983  cnco  17011  cndis  17035  cnindis  17036  cmpsub  17143  hauscmplem  17149  cmpfii  17152  ptcnplem  17331  txtube  17350  txcmplem1  17351  xkoptsub  17364  qtoptop  17407  kqfval  17430  hmeoco  17479  fileln0  17561  trfil1  17597  trfil2  17598  trufil  17621  elfm3  17661  hausflf2  17709  bl2in  17973  metss2lem  18073  metss2  18074  stdbdxmet  18077  metrest  18086  nmfval2  18129  nmval2  18130  nmoix  18254  ioo2bl  18315  xrsxmet  18331  expcn  18392  elcncf  18409  icccvx  18464  iscmet3  18735  causs  18740  metcld2  18748  cmetss  18756  cncmet  18760  bcth3  18769  ovolgelb  18855  ovolfi  18869  shft2rab  18883  uniioombllem3  18956  dyadmax  18969  dyadmbl  18971  subopnmbl  18975  volcn  18977  mbfid  19007  mbfeqalem  19013  mbfres  19015  cnmbf  19030  i1fmulc  19074  mbfi1fseqlem3  19088  mbfi1fseqlem4  19089  itg2seq  19113  itg2gt0  19131  itgss3  19185  dvexp  19318  plypow  19603  plyeq0lem  19608  coeidlem  19635  dgrlt  19663  dgrcolem2  19671  elqaalem2  19716  aacjcl  19723  aaliou3lem1  19738  aaliou3lem2  19739  pserdvlem2  19820  abelthlem8  19831  cosord  19910  sinord  19912  resinf1o  19914  relogexp  19965  logdivlt  19988  advlogexp  20018  logcxp  20032  cxpcl  20037  rpcxpcl  20039  cxpne0  20040  birthdaylem2  20263  cxplim  20282  divsqrsumo1  20294  wilthlem1  20322  ftalem7  20332  basellem1  20334  sgmss  20360  issqf  20390  sqf11  20393  sgmf  20399  sgmnncl  20401  sqff1o  20436  dvdsflsumcom  20444  dvdsmulf1o  20450  sgmppw  20452  chtublem  20466  chtub  20467  logexprlim  20480  bposlem3  20541  bposlem5  20543  bposlem6  20544  lgsdirnn0  20594  lgsquad2  20615  lgsquad3  20616  dchrisumlem1  20654  dchrisumlem2  20655  dchrisumlem3  20656  mulogsumlem  20696  nvo00  21355  nmorepnf  21362  ubthlem1  21465  normpyc  21741  occon3  21892  pjpreeq  21993  idcnop  22577  riesz3i  22658  cnlnssadj  22676  rnbra  22703  strlem3a  22848  cvcon3  22880  ssdmd1  22909  ssdmd2  22910  fzsplit3  23047  esumcst  23451  dmvlsiga  23505  zetacvg  23704  derangsn  23716  iscvm  23805  cvmsval  23812  cvmliftlem7  23837  cvmlift2lem12  23860  supfz  24109  zprod  24160  preduz  24271  predfz  24274  wfrlem10  24336  nobndlem2  24418  brbtwn  24599  bpolylem  24855  bpolysum  24860  bpolydiflem  24861  fsumkthpow  24863  nndivlub  24969  ltflcei  24998  lxflflp1  25000  oprabex2gpop  25139  prmapcp2  25260  repfuntw  25263  isprj2  25267  iintlem1  25713  lvsovso  25729  clscnc  26113  opnrebl2  26339  nn0prpwlem  26341  tailval  26425  fzadd2  26547  caushft  26580  ismtyval  26627  heiborlem7  26644  heiborlem10  26647  heibor  26648  elrfirn  26873  ismrc  26879  nacsfix  26890  mzpcompact2lem  26932  eldiophb  26939  ellz1  26949  rexrabdioph  26978  rpexpmord  27136  congrep  27163  jm2.26a  27196  lindfmm  27400  rngunsnply  27481  mendrng  27603  expgrowthi  27653  4cycl2v2nb  28438  bnj545  29243  bnj929  29284  bnj953  29287
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360
  Copyright terms: Public domain W3C validator