Theorem syl2anr 486

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 485	. 2 |- ( ( ph /\ ta ) -> th )
5	4	ancoms 460	1 |- ( ( ta /\ ph ) -> th )

Syntax hints:   -> wi 4   /\ wa 376

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 190  df-an 378

This theorem is referenced by:  impelOLD  599  swopo  4770  funco  5627  resdif  5848  fvcofneq  6045  fnprb  6139  fntpb  6140  isotr  6245  weisoeq  6264  brrpssg  6592  findsg  6739  coexg  6763  xpexgALT  6805  fnsuppres  6961  wfrlem10  7063  oaass  7280  oeword  7309  oeworde  7312  ixpssmapg  7570  pw2f1olem  7694  domsdomtr  7725  xpen  7753  mapen  7754  mapdom1  7755  mapfienlem1  7936  elfir  7947  wdomen2  8110  carden2b  8419  harcard  8430  isinffi  8444  acnlem  8497  acndom  8500  alephdom  8530  fin23lem21  8787  fin23lem39  8798  isf32lem5  8805  fin1a2lem12  8859  ttukeylem1  8957  pwcfsdom  9026  canthp1  9097  nqereu  9372  addpqf  9387  axmulf  9588  axmulass  9599  axdistr  9600  ltaddnegr  9866  negeu  9885  fimaxre3  10575  nnsub  10670  nn0sub  10944  elz2  10978  uzaddcl  11238  qaddcl  11303  xltneg  11533  xleneg  11534  supxrbnd1  11632  infxrgelb  11646  infmxrgelbOLD  11650  iccneg  11779  uzsubsubfz  11847  fzsplit2  11850  fzss1  11863  uzsplit  11892  fz0fzdiffz0  11925  difelfzle  11929  difelfznle  11930  fvffz0  11934  preduz  11938  predfz  11941  fzonlt0  11968  fzouzsplit  11980  fzo0addelr  11998  eluzgtdifelfzo  12005  elfzodifsumelfzo  12009  ssfzo12  12033  elfznelfzob  12046  fllt  12075  flflp1  12076  uzsup  12123  negmod  12171  modifeq2int  12186  modfzo0difsn  12195  modsumfzodifsn  12196  om2uzlt2i  12203  nn0ennn  12230  suppssfz  12244  seqfveq2  12273  sermono  12283  seqf1o  12292  ser1const  12307  faclbnd  12513  bcval4  12530  bcpasc  12544  hashkf  12555  hashunx  12603  hashfacen  12658  fz1isolem  12665  ishashinf  12667  seqcoll  12668  ccatalpha  12787  swrd0  12844  swrdfv2  12856  swrdspsleq  12859  swrdswrd  12870  swrdccatin12lem2  12899  swrdccat3  12902  revccat  12925  repswswrd  12941  cshwmodn  12951  cshwidxmod  12959  repswcshw  12968  2cshwid  12970  2cshwcom  12972  2cshwcshw  12981  cshwcshid  12983  cshwcsh2id  12984  s1co  12989  cshco  12992  trclub  13139  shftfval  13210  seqshft  13225  crim  13255  caubnd  13498  limsuplt  13615  isercolllem2  13806  fsumcvg  13855  fsumcvg2  13870  fsumshftm  13919  fsumo1  13949  isumshft  13974  harmonic  13994  cvgrat  14016  mertenslem1  14017  zprod  14068  bpolylem  14178  bpolysum  14183  bpolydiflem  14184  fsumkthpow  14186  rpnnen2  14355  dvdsval3  14386  negdvdsb  14396  dvdsnegb  14397  dvdsmul1  14401  odd2np1  14443  divalglem8  14459  ndvdsadd  14468  dvdssqim  14600  nn0seqcvgd  14608  seq1st  14609  algcvgblem  14615  lcmf  14685  lcmfunsnlem2  14692  prmdvdsfz  14728  powm2modprm  14833  modprm0  14835  modprmn0modprm0  14837  pythagtriplem1  14845  pythagtriplem4  14848  pythagtriplem8  14852  pythagtriplem9  14853  pythagtriplem12  14855  pythagtriplem14  14857  pythagtriplem16  14859  pcexp  14888  pc2dvds  14907  pcz  14909  fldivp1  14921  pcfac  14923  pockthg  14929  infpnlem1  14933  prmreclem1  14939  prmreclem2  14940  1arith  14950  4sqlem11  14978  vdwlem2  15011  vdwlem8  15017  vdwnnlem2  15025  prmgaplem7  15106  prmgaplem8  15107  cshwshashlem2  15145  cshwshashlem3  15146  pwsval  15462  isacs1i  15641  funcsetcestrclem9  16126  ismgmid  16585  mhmpropd  16666  grpsubid1  16817  mulgnnp1  16844  mulgsubcl  16850  mulgnn0z  16856  mulgnndir  16858  mulgneg2  16863  lagsubg  16957  ghmco  16980  symg2bas  17117  symgextfv  17137  pgpfi2  17336  efgsfo  17467  frgpupf  17501  frgpup1  17503  gsummptshft  17647  telgsumfzslem  17696  telgsums  17701  ablfac1eu  17784  pgpfac1lem2  17786  ablfaclem3  17798  dvdsrid  17957  dvdsrneg  17960  dvr1  17995  abv1  18139  lbsexg  18465  gsummoncoe1  18975  xrsds  19088  znf1o  19199  lindfmm  19462  matecl  19527  mavmul0g  19655  gsummatr01  19761  mp2pm2mplem4  19910  chfacfisf  19955  chfacfisfcpmat  19956  chfacfpmmulgsum2  19966  cpmadugsumlemF  19977  isclo  20180  resttopon  20254  restcld  20265  restcls  20274  iscn  20328  iscnp  20330  cnco  20359  cndis  20384  cnindis  20385  cmpsub  20492  hauscmplem  20498  cmpfii  20501  ptcnplem  20713  txtube  20732  txcmplem1  20733  xkoptsub  20746  qtoptop  20792  kqfval  20815  hmeoco  20864  fileln0  20943  trfil1  20979  trfil2  20980  trufil  21003  elfm3  21043  hausflf2  21091  isucn  21371  bl2in  21493  metss2lem  21604  metss2  21605  stdbdxmet  21608  metrest  21617  nmfval2  21683  nmval2  21684  nmoix  21812  nmoixOLD  21828  ioo2bl  21889  xrsxmet  21905  expcn  21982  elcncf  21999  icccvx  22056  iscmet3  22341  causs  22346  metcld2  22354  cmetss  22362  cncmet  22368  bcth3  22377  ovolgelb  22511  ovolfi  22525  shft2rab  22539  uniioombllem3  22622  dyadmax  22635  dyadmbl  22637  subopnmbl  22641  volcn  22643  mbfid  22671  mbfeqalem  22677  mbfres  22679  cnmbf  22694  i1fmulc  22740  mbfi1fseqlem3  22754  mbfi1fseqlem4  22755  itg2seq  22779  itg2gt0  22797  itgss3  22851  dvexp  22986  plypow  23238  plyeq0lem  23243  coeidlem  23270  dgrlt  23299  dgrcolem2  23307  elqaalem2  23352  elqaalem2OLD  23355  aacjcl  23362  aaliou3lem1  23377  aaliou3lem2  23378  pserdvlem2  23462  abelthlem8  23473  cosord  23560  sinord  23562  resinf1o  23564  relogexp  23624  logdivlt  23649  advlogexp  23679  logcxp  23693  cxpcl  23698  rpcxpcl  23700  cxpne0  23701  logbchbase  23787  birthdaylem2  23957  cxplim  23976  divsqrtsumo1  23988  zetacvg  24019  wilthlem1  24072  ftalem7  24084  basellem1  24086  sgmss  24112  issqf  24142  sqf11  24145  sgmf  24151  sgmnncl  24153  sqff1o  24188  dvdsflsumcom  24196  dvdsmulf1o  24202  sgmppw  24204  chtublem  24218  chtub  24219  logexprlim  24232  bposlem3  24293  bposlem5  24295  bposlem6  24296  lgsdirnn0  24346  lgsquad2  24367  lgsquad3  24368  dchrisumlem1  24406  dchrisumlem2  24407  dchrisumlem3  24408  mulogsumlem  24448  brbtwn  25008  usgrafilem2  25219  cusgraexi  25275  cusgrafilem2  25287  usgra2wlkspthlem2  25427  vfwlkniswwlkn  25513  clwlkisclwwlklem2fv2  25590  hashnbgravdg  25720  nbhashuvtx1  25722  rusgranumwlk  25764  4cycl2v2nb  25823  frg2woteqm  25866  2spotmdisj  25875  extwwlkfablem1  25881  numclwwlk8  25922  nvo00  26483  nmorepnf  26490  ubthlem1  26593  normpyc  26880  occon3  27031  pjpreeq  27132  idcnop  27715  riesz3i  27796  cnlnssadj  27814  rnbra  27841  strlem3a  27986  cvcon3  28018  ssdmd1  28047  ssdmd2  28048  relfi  28289  fzsplit3  28445  esumcst  28958  dmvlsiga  29025  ballotlemimin  29411  ballotlemiminOLD  29449  bnj545  29778  bnj929  29819  bnj953  29822  derangsn  29965  iscvm  30054  cvmsval  30061  cvmliftlem7  30086  cvmlift2lem12  30109  mclsssvlem  30272  supfz  30434  faclimlem3  30452  nobndlem2  30653  opnrebl2  31048  nn0prpwlem  31049  tailval  31100  nndivlub  31189  finixpnum  31994  ltflcei  31997  poimirlem4  32008  poimirlem14  32018  poimirlem15  32019  poimirlem19  32023  poimirlem20  32024  poimirlem22  32026  poimirlem24  32028  poimirlem28  32032  poimirlem30  32034  poimirlem31  32035  mblfinlem2  32042  mblfinlem3  32043  mblfinlem4  32044  ftc1anclem1  32081  ftc1anclem4  32084  ftc1anclem5  32085  ftc1anclem7  32087  ftc1anclem8  32088  ftc1anc  32089  fzadd2  32134  caushft  32154  ismtyval  32196  heiborlem7  32213  heiborlem10  32216  heibor  32217  elrfirn  35608  ismrc  35614  nacsfix  35625  mzpcompact2lem  35664  eldiophb  35670  ellz1  35680  rexrabdioph  35708  rpexpmord  35867  congrep  35894  jm2.26a  35926  rngunsnply  36110  mendring  36129  iocmbl  36168  rp-isfinite5  36233  isprm7  36730  expgrowthi  36752  cnfex  37412  icccncfext  37862  itgsinexp  37928  iblspltprt  37947  itgspltprt  37953  fourierdlem50  38132  fourierswlem  38206  etransclem35  38246  iccpartres  38877  iccelpart  38892  iccpartiun  38893  iccpartnel  38897  sgoldbaltlem2  39026  bgoldbachlt  39051  addlenpfx  39086  pfxccatin12lem2  39112  pfxccat3  39114  zm1nn  39194  ltsubnn0  39196  subsubelfzo0  39207  uspgrupgrushgr  39425  usgrumgruspgr  39428  cusgrfilem2  39682  upgr1wlkwlk  39842  crctcsh1wlkn0lem4  39991  crctcsh1wlkn0lem6  39993  crctcsh1wlkn0lem7  39994  crctcsh1wlkn0  39999  is01wlk  40007  is0Trl  40012  mgmhmpropd  40293  2zrngamgm  40447  lincresunit3  40782  lincreslvec3  40783  isldepslvec2  40786  m1modmmod  40832  blengt1fldiv2p1  40912  dignn0flhalf  40937  nn0sumshdiglemA  40938  aacllem  41046