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  4324  findsg  4683  coexg  5215  funco  5292  resdif  5494  fnsuppres  5732  isotr  5833  weisoeq  5853  xpexgALT  6070  brrpssg  6279  oaass  6559  oeword  6588  oeworde  6591  ixpssmapg  6846  pw2f1olem  6966  domsdomtr  6996  xpen  7024  mapen  7025  mapdom1  7026  elfir  7169  wdomen2  7291  carden2b  7600  harcard  7611  isinffi  7625  acnlem  7675  acndom  7678  alephdom  7708  fin23lem21  7965  fin23lem39  7976  isf32lem5  7983  fin1a2lem12  8037  ttukeylem1  8136  pwcfsdom  8205  canthp1  8276  nqereu  8553  addpqf  8568  axmulf  8768  axmulass  8779  axdistr  8780  negeu  9042  fimaxre3  9703  nnsub  9784  nn0sub  10014  elz2  10040  uzaddcl  10275  qaddcl  10332  xltneg  10544  xleneg  10545  supxrbnd1  10640  infmxrgelb  10653  iccneg  10757  fzsplit2  10815  fzss1  10830  uzsplit  10855  fzm1  10862  fzouzsplit  10901  fllt  10938  uzsup  10967  om2uzlt2i  11014  nn0ennn  11041  seqfveq2  11068  sermono  11078  seqf1o  11087  ser1const  11102  faclbnd  11303  bcval4  11320  bcpasc  11333  hashkf  11339  hashfacen  11392  fz1isolem  11399  seqcoll  11401  revccat  11484  s1co  11488  shftfval  11565  seqshft  11580  crim  11600  caubnd  11842  isercolllem2  12139  fsumcvg  12185  zsum  12191  fsumcvg2  12200  fsumshftm  12243  fsumo1  12270  isumshft  12298  harmonic  12317  cvgrat  12339  mertenslem1  12340  rpnnen2  12504  dvdsval3  12535  negdvdsb  12545  dvdsnegb  12546  dvdsmul1  12550  odd2np1  12587  divalglem8  12599  ndvdsadd  12607  dvdssqim  12732  nn0seqcvgd  12740  seq1st  12741  algcvgblem  12747  pythagtriplem1  12869  pythagtriplem4  12872  pythagtriplem8  12876  pythagtriplem9  12877  pythagtriplem12  12879  pythagtriplem14  12881  pythagtriplem16  12883  pcexp  12912  pc2dvds  12931  pcz  12933  fldivp1  12945  pcfac  12947  pockthg  12953  infpnlem1  12957  prmreclem1  12963  prmreclem2  12964  1arith  12974  4sqlem11  13002  vdwlem2  13029  vdwlem8  13035  vdwnnlem2  13043  pwsval  13385  isacs1i  13559  ismgmid  14387  mhmpropd  14421  grpsubid1  14551  mulgnnp1  14575  mulgsubcl  14581  mulgnn0z  14587  mulgnndir  14589  mulgneg2  14594  lagsubg  14679  ghmco  14702  pgpfi2  14917  efgsfo  15048  frgpup1  15084  ablfac1eu  15308  pgpfac1lem2  15310  ablfaclem3  15322  dvdsrid  15433  dvdsrneg  15436  dvr1  15471  abv1  15598  lbsexg  15917  xrsds  16414  znf1o  16505  isclo  16824  resttopon  16892  restcld  16903  restcls  16911  iscn  16965  iscnp  16967  cnco  16995  cndis  17019  cnindis  17020  cmpsub  17127  hauscmplem  17133  cmpfii  17136  ptcnplem  17315  txtube  17334  txcmplem1  17335  xkoptsub  17348  qtoptop  17391  kqfval  17414  hmeoco  17463  fileln0  17545  trfil1  17581  trfil2  17582  trufil  17605  elfm3  17645  hausflf2  17693  bl2in  17957  metss2lem  18057  metss2  18058  stdbdxmet  18061  metrest  18070  nmfval2  18113  nmval2  18114  nmoix  18238  ioo2bl  18299  xrsxmet  18315  expcn  18376  elcncf  18393  icccvx  18448  iscmet3  18719  causs  18724  metcld2  18732  cmetss  18740  cncmet  18744  bcth3  18753  ovolgelb  18839  ovolfi  18853  shft2rab  18867  uniioombllem3  18940  dyadmax  18953  dyadmbl  18955  subopnmbl  18959  volcn  18961  mbfid  18991  mbfeqalem  18997  mbfres  18999  cnmbf  19014  i1fmulc  19058  mbfi1fseqlem3  19072  mbfi1fseqlem4  19073  itg2seq  19097  itg2gt0  19115  itgss3  19169  dvexp  19302  plypow  19587  plyeq0lem  19592  coeidlem  19619  dgrlt  19647  dgrcolem2  19655  elqaalem2  19700  aacjcl  19707  aaliou3lem1  19722  aaliou3lem2  19723  pserdvlem2  19804  abelthlem8  19815  cosord  19894  sinord  19896  resinf1o  19898  relogexp  19949  logdivlt  19972  advlogexp  20002  logcxp  20016  cxpcl  20021  rpcxpcl  20023  cxpne0  20024  birthdaylem2  20247  cxplim  20266  divsqrsumo1  20278  wilthlem1  20306  ftalem7  20316  basellem1  20318  sgmss  20344  issqf  20374  sqf11  20377  sgmf  20383  sgmnncl  20385  sqff1o  20420  dvdsflsumcom  20428  dvdsmulf1o  20434  sgmppw  20436  chtublem  20450  chtub  20451  logexprlim  20464  bposlem3  20525  bposlem5  20527  bposlem6  20528  lgsdirnn0  20578  lgsquad2  20599  lgsquad3  20600  dchrisumlem1  20638  dchrisumlem2  20639  dchrisumlem3  20640  mulogsumlem  20680  nvo00  21339  nmorepnf  21346  ubthlem1  21449  normpyc  21725  occon3  21876  pjpreeq  21977  idcnop  22561  riesz3i  22642  cnlnssadj  22660  rnbra  22687  strlem3a  22832  cvcon3  22864  ssdmd1  22893  ssdmd2  22894  fzsplit3  23031  zetacvg  23100  derangsn  23112  iscvm  23201  cvmsval  23208  cvmliftlem7  23233  cvmlift2lem12  23256  supfz  23505  preduz  23611  predfz  23614  wfrlem10  23676  nobndlem2  23758  brbtwn  23938  bpolylem  24194  bpolysum  24199  bpolydiflem  24200  fsumkthpow  24202  nndivlub  24308  oprabex2gpop  24448  prmapcp2  24569  isprj2  24576  iintlem1  25022  lvsovso  25038  clscnc  25422  opnrebl2  25648  nn0prpwlem  25650  tailval  25734  fzadd2  25856  caushft  25889  ismtyval  25936  heiborlem7  25953  heiborlem10  25956  heibor  25957  elrfirn  26182  ismrc  26188  nacsfix  26199  mzpcompact2lem  26241  eldiophb  26248  ellz1  26258  rexrabdioph  26287  rpexpmord  26445  congrep  26472  jm2.26a  26505  lindfmm  26709  rngunsnply  26790  mendrng  26912  expgrowthi  26962  bnj545  28300  bnj929  28341  bnj953  28344
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