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  4784  funco  5639  resdif  5851  fvcofneq  6045  fnprb  6138  isotr  6242  weisoeq  6261  brrpssg  6587  findsg  6734  coexg  6758  xpexgALT  6800  fnsuppres  6953  wfrlem10  7056  oaass  7273  oeword  7302  oeworde  7305  ixpssmapg  7563  pw2f1olem  7685  domsdomtr  7716  xpen  7744  mapen  7745  mapdom1  7746  mapfienlem1  7927  elfir  7938  wdomen2  8101  carden2b  8409  harcard  8420  isinffi  8434  acnlem  8486  acndom  8489  alephdom  8519  fin23lem21  8776  fin23lem39  8787  isf32lem5  8794  fin1a2lem12  8848  ttukeylem1  8946  pwcfsdom  9015  canthp1  9086  nqereu  9361  addpqf  9376  axmulf  9577  axmulass  9588  axdistr  9589  negeu  9872  fimaxre3  10560  nnsub  10655  nn0sub  10927  elz2  10961  uzaddcl  11222  qaddcl  11287  xltneg  11517  xleneg  11518  supxrbnd1  11614  infxrgelb  11628  infmxrgelbOLD  11632  iccneg  11760  uzsubsubfz  11828  fzsplit2  11831  fzss1  11844  uzsplit  11873  fz0fzdiffz0  11906  difelfzle  11911  difelfznle  11912  preduz  11918  predfz  11921  fzonlt0  11948  fzouzsplit  11960  fzo0addelr  11975  eluzgtdifelfzo  11982  elfzodifsumelfzo  11986  ssfzo12  12010  elfznelfzob  12021  fllt  12048  flflp1  12049  uzsup  12096  negmod  12144  modifeq2int  12158  om2uzlt2i  12171  nn0ennn  12198  suppssfz  12212  seqfveq2  12241  sermono  12251  seqf1o  12260  ser1const  12275  faclbnd  12481  bcval4  12498  bcpasc  12512  hashkf  12523  hashunx  12571  hashfacen  12621  fz1isolem  12628  ishashinf  12630  seqcoll  12631  swrd0  12792  swrdfv2  12804  swrdspsleq  12807  swrdswrd  12818  swrdccatin12lem2  12847  swrdccat3  12850  revccat  12873  repswswrd  12889  cshwmodn  12899  cshwidxmod  12907  repswcshw  12913  2cshwid  12915  2cshwcom  12917  2cshwcshw  12926  cshwcshid  12928  cshwcsh2id  12929  s1co  12932  cshco  12935  trclub  13062  shftfval  13133  seqshft  13148  crim  13178  caubnd  13421  limsuplt  13537  isercolllem2  13728  fsumcvg  13777  fsumcvg2  13792  fsumshftm  13841  fsumo1  13871  isumshft  13896  harmonic  13916  cvgrat  13938  mertenslem1  13939  zprod  13990  bpolylem  14100  bpolysum  14105  bpolydiflem  14106  fsumkthpow  14108  rpnnen2  14277  dvdsval3  14308  negdvdsb  14318  dvdsnegb  14319  dvdsmul1  14323  odd2np1  14364  divalglem8  14379  ndvdsadd  14388  dvdssqim  14520  nn0seqcvgd  14528  seq1st  14529  algcvgblem  14535  lcmf  14605  lcmfunsnlem2  14612  prmdvdsfz  14648  powm2modprm  14753  modprm0  14755  modprmn0modprm0  14757  pythagtriplem1  14765  pythagtriplem4  14768  pythagtriplem8  14772  pythagtriplem9  14773  pythagtriplem12  14775  pythagtriplem14  14777  pythagtriplem16  14779  pcexp  14808  pc2dvds  14827  pcz  14829  fldivp1  14841  pcfac  14843  pockthg  14849  infpnlem1  14853  prmreclem1  14859  prmreclem2  14860  1arith  14870  4sqlem11  14898  vdwlem2  14931  vdwlem8  14937  vdwnnlem2  14945  prmgaplem7  15026  prmgaplem8  15027  cshwshashlem2  15066  cshwshashlem3  15067  pwsval  15383  isacs1i  15562  funcsetcestrclem9  16047  ismgmid  16506  mhmpropd  16587  grpsubid1  16738  mulgnnp1  16765  mulgsubcl  16771  mulgnn0z  16777  mulgnndir  16779  mulgneg2  16784  lagsubg  16878  ghmco  16901  symg2bas  17038  symgextfv  17058  pgpfi2  17257  efgsfo  17388  frgpupf  17422  frgpup1  17424  gsummptshft  17568  telgsumfzslem  17617  telgsums  17622  ablfac1eu  17705  pgpfac1lem2  17707  ablfaclem3  17719  dvdsrid  17878  dvdsrneg  17881  dvr1  17916  abv1  18060  lbsexg  18386  gsummoncoe1  18897  xrsds  19010  znf1o  19120  lindfmm  19383  matecl  19448  mavmul0g  19576  gsummatr01  19682  mp2pm2mplem4  19831  chfacfisf  19876  chfacfisfcpmat  19877  chfacfpmmulgsum2  19887  cpmadugsumlemF  19898  isclo  20101  resttopon  20175  restcld  20186  restcls  20195  iscn  20249  iscnp  20251  cnco  20280  cndis  20305  cnindis  20306  cmpsub  20413  hauscmplem  20419  cmpfii  20422  ptcnplem  20634  txtube  20653  txcmplem1  20654  xkoptsub  20667  qtoptop  20713  kqfval  20736  hmeoco  20785  fileln0  20863  trfil1  20899  trfil2  20900  trufil  20923  elfm3  20963  hausflf2  21011  isucn  21291  bl2in  21413  metss2lem  21524  metss2  21525  stdbdxmet  21528  metrest  21537  nmfval2  21603  nmval2  21604  nmoix  21732  nmoixOLD  21748  ioo2bl  21809  xrsxmet  21825  expcn  21902  elcncf  21919  icccvx  21976  iscmet3  22261  causs  22266  metcld2  22274  cmetss  22282  cncmet  22288  bcth3  22297  ovolgelb  22431  ovolfi  22445  shft2rab  22459  uniioombllem3  22541  dyadmax  22554  dyadmbl  22556  subopnmbl  22560  volcn  22562  mbfid  22590  mbfeqalem  22596  mbfres  22598  cnmbf  22613  i1fmulc  22659  mbfi1fseqlem3  22673  mbfi1fseqlem4  22674  itg2seq  22698  itg2gt0  22716  itgss3  22770  dvexp  22905  plypow  23157  plyeq0lem  23162  coeidlem  23189  dgrlt  23218  dgrcolem2  23226  elqaalem2  23271  elqaalem2OLD  23274  aacjcl  23281  aaliou3lem1  23296  aaliou3lem2  23297  pserdvlem2  23381  abelthlem8  23392  cosord  23479  sinord  23481  resinf1o  23483  relogexp  23543  logdivlt  23568  advlogexp  23598  logcxp  23612  cxpcl  23617  rpcxpcl  23619  cxpne0  23620  logbchbase  23706  birthdaylem2  23876  cxplim  23895  divsqrtsumo1  23907  zetacvg  23938  wilthlem1  23991  ftalem7  24003  basellem1  24005  sgmss  24031  issqf  24061  sqf11  24064  sgmf  24070  sgmnncl  24072  sqff1o  24107  dvdsflsumcom  24115  dvdsmulf1o  24121  sgmppw  24123  chtublem  24137  chtub  24138  logexprlim  24151  bposlem3  24212  bposlem5  24214  bposlem6  24215  lgsdirnn0  24265  lgsquad2  24286  lgsquad3  24287  dchrisumlem1  24325  dchrisumlem2  24326  dchrisumlem3  24327  mulogsumlem  24367  brbtwn  24927  usgrafilem2  25138  cusgraexi  25194  cusgrafilem2  25206  usgra2wlkspthlem2  25346  vfwlkniswwlkn  25432  clwlkisclwwlklem2fv2  25509  hashnbgravdg  25639  nbhashuvtx1  25641  rusgranumwlk  25683  4cycl2v2nb  25742  frg2woteqm  25785  2spotmdisj  25794  extwwlkfablem1  25800  numclwwlk8  25841  nvo00  26400  nmorepnf  26407  ubthlem1  26510  normpyc  26797  occon3  26948  pjpreeq  27049  idcnop  27632  riesz3i  27713  cnlnssadj  27731  rnbra  27758  strlem3a  27903  cvcon3  27935  ssdmd1  27964  ssdmd2  27965  relfi  28215  fzsplit3  28376  esumcst  28892  dmvlsiga  28959  ballotlemimin  29346  ballotlemiminOLD  29384  bnj545  29714  bnj929  29755  bnj953  29758  derangsn  29901  iscvm  29990  cvmsval  29997  cvmliftlem7  30022  cvmlift2lem12  30045  mclsssvlem  30208  supfz  30369  faclimlem3  30388  nobndlem2  30587  opnrebl2  30982  nn0prpwlem  30983  tailval  31034  nndivlub  31123  finixpnum  31894  ltflcei  31897  poimirlem4  31908  poimirlem14  31918  poimirlem15  31919  poimirlem19  31923  poimirlem20  31924  poimirlem22  31926  poimirlem24  31928  poimirlem28  31932  poimirlem30  31934  poimirlem31  31935  mblfinlem2  31942  mblfinlem3  31943  mblfinlem4  31944  ftc1anclem1  31981  ftc1anclem4  31984  ftc1anclem5  31985  ftc1anclem7  31987  ftc1anclem8  31988  ftc1anc  31989  fzadd2  32034  caushft  32054  ismtyval  32096  heiborlem7  32113  heiborlem10  32116  heibor  32117  elrfirn  35506  ismrc  35512  nacsfix  35523  mzpcompact2lem  35562  eldiophb  35568  ellz1  35578  rexrabdioph  35606  rpexpmord  35766  congrep  35793  jm2.26a  35825  rngunsnply  36009  mendring  36028  iocmbl  36067  rp-isfinite5  36132  isprm7  36630  expgrowthi  36652  cnfex  37322  icccncfext  37705  itgsinexp  37771  iblspltprt  37790  itgspltprt  37796  fourierdlem50  37960  fourierswlem  38034  etransclem35  38074  iccpartres  38602  iccelpart  38617  iccpartiun  38618  iccpartnel  38622  sgoldbaltlem2  38751  bgoldbachlt  38776  addlenpfx  38809  pfxccatin12lem2  38835  pfxccat3  38837  zm1nn  38903  ltsubnn0  38905  subsubelfzo0  38916  cusgrfilem2  39273  mgmhmpropd  39404  2zrngamgm  39558  lincresunit3  39895  lincreslvec3  39896  isldepslvec2  39899  m1modmmod  39945  blengt1fldiv2p1  40025  dignn0flhalf  40050  nn0sumshdiglemA  40051  aacllem  40161