Theorem syl2anr 480

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

Step	Hyp	Ref	Expression
1		syl2an.1	. . 3 |- ( ph -> ps )
2		syl2an.2	. . 3 |- ( ta -> ch )
3		syl2an.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	1, 2, 3	syl2an 479	. 2 |- ( ( ph /\ ta ) -> th )
5	4	ancoms 454	1 |- ( ( ta /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 370

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 188  df-an 372

This theorem is referenced by:  impelOLD  591  swopo  4785  funco  5639  resdif  5851  fvcofneq  6045  fnprb  6138  isotr  6242  weisoeq  6261  brrpssg  6587  findsg  6734  coexg  6758  xpexgALT  6800  fnsuppres  6953  wfrlem10  7053  oaass  7270  oeword  7299  oeworde  7302  ixpssmapg  7560  pw2f1olem  7682  domsdomtr  7713  xpen  7741  mapen  7742  mapdom1  7743  mapfienlem1  7924  elfir  7935  wdomen2  8092  carden2b  8400  harcard  8411  isinffi  8425  acnlem  8477  acndom  8480  alephdom  8510  fin23lem21  8767  fin23lem39  8778  isf32lem5  8785  fin1a2lem12  8839  ttukeylem1  8937  pwcfsdom  9006  canthp1  9078  nqereu  9353  addpqf  9368  axmulf  9569  axmulass  9580  axdistr  9581  negeu  9864  fimaxre3  10553  nnsub  10648  nn0sub  10920  elz2  10954  uzaddcl  11215  qaddcl  11280  xltneg  11510  xleneg  11511  supxrbnd1  11607  infxrgelb  11621  infmxrgelbOLD  11625  iccneg  11751  uzsubsubfz  11819  fzsplit2  11822  fzss1  11835  uzsplit  11864  fz0fzdiffz0  11897  difelfzle  11902  difelfznle  11903  preduz  11909  predfz  11912  fzonlt0  11939  fzouzsplit  11951  fzo0addelr  11966  eluzgtdifelfzo  11973  elfzodifsumelfzo  11977  ssfzo12  12001  elfznelfzob  12012  fllt  12039  flflp1  12040  uzsup  12087  negmod  12135  modifeq2int  12149  om2uzlt2i  12162  nn0ennn  12189  suppssfz  12203  seqfveq2  12232  sermono  12242  seqf1o  12251  ser1const  12266  faclbnd  12472  bcval4  12489  bcpasc  12503  hashkf  12514  hashunx  12562  hashfacen  12612  fz1isolem  12619  seqcoll  12621  hash2prd  12627  swrd0  12775  swrdfv2  12787  swrdspsleq  12790  swrdswrd  12801  swrdccatin12lem2  12830  swrdccat3  12833  revccat  12856  repswswrd  12872  cshwmodn  12882  cshwidxmod  12890  repswcshw  12896  2cshwid  12898  2cshwcom  12900  2cshwcshw  12909  cshwcshid  12911  cshwcsh2id  12912  s1co  12915  cshco  12918  trclub  13041  shftfval  13112  seqshft  13127  crim  13157  caubnd  13400  limsuplt  13516  isercolllem2  13707  fsumcvg  13756  fsumcvg2  13771  fsumshftm  13820  fsumo1  13850  isumshft  13875  harmonic  13895  cvgrat  13917  mertenslem1  13918  zprod  13969  bpolylem  14079  bpolysum  14084  bpolydiflem  14085  fsumkthpow  14087  rpnnen2  14256  dvdsval3  14287  negdvdsb  14297  dvdsnegb  14298  dvdsmul1  14302  odd2np1  14343  divalglem8  14356  ndvdsadd  14364  dvdssqim  14492  nn0seqcvgd  14500  seq1st  14501  algcvgblem  14507  lcmf  14568  lcmfunsnlem2  14575  prmdvdsfz  14611  powm2modprm  14708  modprm0  14710  modprmn0modprm0  14712  pythagtriplem1  14720  pythagtriplem4  14723  pythagtriplem8  14727  pythagtriplem9  14728  pythagtriplem12  14730  pythagtriplem14  14732  pythagtriplem16  14734  pcexp  14763  pc2dvds  14782  pcz  14784  fldivp1  14796  pcfac  14798  pockthg  14804  infpnlem1  14808  prmreclem1  14814  prmreclem2  14815  1arith  14825  4sqlem11  14853  vdwlem2  14886  vdwlem8  14892  vdwnnlem2  14900  prmgaplem7  14981  prmgaplem8  14982  cshwshashlem2  15021  cshwshashlem3  15022  pwsval  15334  isacs1i  15505  funcsetcestrclem9  15990  ismgmid  16449  mhmpropd  16530  grpsubid1  16681  mulgnnp1  16708  mulgsubcl  16714  mulgnn0z  16720  mulgnndir  16722  mulgneg2  16727  lagsubg  16821  ghmco  16844  symg2bas  16981  symgextfv  17001  pgpfi2  17184  efgsfo  17315  frgpupf  17349  frgpup1  17351  gsummptshft  17495  telgsumfzslem  17544  telgsums  17549  ablfac1eu  17632  pgpfac1lem2  17634  ablfaclem3  17646  dvdsrid  17805  dvdsrneg  17808  dvr1  17843  abv1  17987  lbsexg  18313  gsummoncoe1  18824  xrsds  18937  znf1o  19044  lindfmm  19307  matecl  19372  mavmul0g  19500  gsummatr01  19606  mp2pm2mplem4  19755  chfacfisf  19800  chfacfisfcpmat  19801  chfacfpmmulgsum2  19811  cpmadugsumlemF  19822  isclo  20025  resttopon  20099  restcld  20110  restcls  20119  iscn  20173  iscnp  20175  cnco  20204  cndis  20229  cnindis  20230  cmpsub  20337  hauscmplem  20343  cmpfii  20346  ptcnplem  20558  txtube  20577  txcmplem1  20578  xkoptsub  20591  qtoptop  20637  kqfval  20660  hmeoco  20709  fileln0  20787  trfil1  20823  trfil2  20824  trufil  20847  elfm3  20887  hausflf2  20935  isucn  21215  bl2in  21337  metss2lem  21448  metss2  21449  stdbdxmet  21452  metrest  21461  nmfval2  21527  nmval2  21528  nmoix  21652  ioo2bl  21713  xrsxmet  21729  expcn  21791  elcncf  21808  icccvx  21865  iscmet3  22147  causs  22152  metcld2  22160  cmetss  22168  cncmet  22174  bcth3  22183  ovolgelb  22302  ovolfi  22316  shft2rab  22330  uniioombllem3  22411  dyadmax  22424  dyadmbl  22426  subopnmbl  22430  volcn  22432  mbfid  22460  mbfeqalem  22466  mbfres  22468  cnmbf  22483  i1fmulc  22529  mbfi1fseqlem3  22543  mbfi1fseqlem4  22544  itg2seq  22568  itg2gt0  22586  itgss3  22640  dvexp  22775  plypow  23018  plyeq0lem  23023  coeidlem  23050  dgrlt  23079  dgrcolem2  23087  elqaalem2  23132  aacjcl  23139  aaliou3lem1  23154  aaliou3lem2  23155  pserdvlem2  23239  abelthlem8  23250  cosord  23337  sinord  23339  resinf1o  23341  relogexp  23401  logdivlt  23426  advlogexp  23456  logcxp  23470  cxpcl  23475  rpcxpcl  23477  cxpne0  23478  logbchbase  23564  birthdaylem2  23734  cxplim  23753  divsqrtsumo1  23765  zetacvg  23796  wilthlem1  23849  ftalem7  23859  basellem1  23861  sgmss  23887  issqf  23917  sqf11  23920  sgmf  23926  sgmnncl  23928  sqff1o  23963  dvdsflsumcom  23971  dvdsmulf1o  23977  sgmppw  23979  chtublem  23993  chtub  23994  logexprlim  24007  bposlem3  24068  bposlem5  24070  bposlem6  24071  lgsdirnn0  24121  lgsquad2  24142  lgsquad3  24143  dchrisumlem1  24181  dchrisumlem2  24182  dchrisumlem3  24183  mulogsumlem  24223  brbtwn  24766  usgrafilem2  24976  cusgraexi  25032  cusgrafilem2  25044  usgra2wlkspthlem2  25184  vfwlkniswwlkn  25270  clwlkisclwwlklem2fv2  25347  hashnbgravdg  25477  nbhashuvtx1  25479  rusgranumwlk  25521  4cycl2v2nb  25580  frg2woteqm  25623  2spotmdisj  25632  extwwlkfablem1  25638  numclwwlk8  25679  nvo00  26238  nmorepnf  26245  ubthlem1  26348  normpyc  26625  occon3  26776  pjpreeq  26877  idcnop  27460  riesz3i  27541  cnlnssadj  27559  rnbra  27586  strlem3a  27731  cvcon3  27763  ssdmd1  27792  ssdmd2  27793  relfi  28043  fzsplit3  28197  ishashinf  28208  esumcst  28714  dmvlsiga  28781  ballotlemimin  29155  bnj545  29485  bnj929  29526  bnj953  29529  derangsn  29672  iscvm  29761  cvmsval  29768  cvmliftlem7  29793  cvmlift2lem12  29816  mclsssvlem  29979  supfz  30140  faclimlem3  30159  nobndlem2  30358  opnrebl2  30753  nn0prpwlem  30754  tailval  30805  nndivlub  30894  finixpnum  31624  ltflcei  31627  poimirlem4  31638  poimirlem14  31648  poimirlem15  31649  poimirlem19  31653  poimirlem20  31654  poimirlem22  31656  poimirlem24  31658  poimirlem28  31662  poimirlem30  31664  poimirlem31  31665  mblfinlem2  31672  mblfinlem3  31673  mblfinlem4  31674  ftc1anclem1  31711  ftc1anclem4  31714  ftc1anclem5  31715  ftc1anclem7  31717  ftc1anclem8  31718  ftc1anc  31719  fzadd2  31764  caushft  31784  ismtyval  31826  heiborlem7  31843  heiborlem10  31846  heibor  31847  elrfirn  35236  ismrc  35242  nacsfix  35253  mzpcompact2lem  35292  eldiophb  35298  ellz1  35308  rexrabdioph  35336  rpexpmord  35492  congrep  35519  jm2.26a  35551  rngunsnply  35728  mendring  35747  iocmbl  35786  rp-isfinite5  35851  isprm7  36287  expgrowthi  36309  cnfex  36979  icccncfext  37327  itgsinexp  37390  iblspltprt  37409  itgspltprt  37415  fourierdlem50  37578  fourierswlem  37652  etransclem35  37691  iccpartres  38112  iccelpart  38127  iccpartiun  38128  iccpartnel  38132  sgoldbaltlem2  38261  bgoldbachlt  38286  addlenpfx  38319  pfxccatin12lem2  38345  pfxccat3  38347  zm1nn  38388  ltsubnn0  38390  subsubelfzo0  38401  mgmhmpropd  38533  2zrngamgm  38687  lincresunit3  39024  lincreslvec3  39025  isldepslvec2  39028  m1modmmod  39075  blengt1fldiv2p1  39155  dignn0flhalf  39180  nn0sumshdiglemA  39181  aacllem  39291