Theorem syl2anr 465

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

Syntax hints:   -> wi 4   /\ wa 359

This theorem is referenced by:  swopo  4473  findsg  4831  coexg  5371  funco  5450  resdif  5655  fnpr  5909  fnprOLD  5910  fnsuppres  5911  isotr  6015  weisoeq  6035  xpexgALT  6256  brrpssg  6483  oaass  6763  oeword  6792  oeworde  6795  ixpssmapg  7051  pw2f1olem  7171  domsdomtr  7201  xpen  7229  mapen  7230  mapdom1  7231  elfir  7378  wdomen2  7501  carden2b  7810  harcard  7821  isinffi  7835  acnlem  7885  acndom  7888  alephdom  7918  fin23lem21  8175  fin23lem39  8186  isf32lem5  8193  fin1a2lem12  8247  ttukeylem1  8345  pwcfsdom  8414  canthp1  8485  nqereu  8762  addpqf  8777  axmulf  8977  axmulass  8988  axdistr  8989  negeu  9252  fimaxre3  9913  nnsub  9994  nn0sub  10226  elz2  10254  uzaddcl  10489  qaddcl  10546  xltneg  10759  xleneg  10760  supxrbnd1  10856  infmxrgelb  10869  iccneg  10974  fzsplit2  11032  fzss1  11047  uzsplit  11073  fzm1  11082  fzouzsplit  11123  elfznelfzob  11148  fllt  11170  uzsup  11199  om2uzlt2i  11246  nn0ennn  11273  seqfveq2  11300  sermono  11310  seqf1o  11319  ser1const  11334  faclbnd  11536  bcval4  11553  bcpasc  11567  hashkf  11575  hashunx  11615  hashfacen  11658  fz1isolem  11665  seqcoll  11667  revccat  11753  s1co  11757  shftfval  11840  seqshft  11855  crim  11875  caubnd  12117  isercolllem2  12414  fsumcvg  12461  zsum  12467  fsumcvg2  12476  fsumshftm  12519  fsumo1  12546  isumshft  12574  harmonic  12593  cvgrat  12615  mertenslem1  12616  rpnnen2  12780  dvdsval3  12811  negdvdsb  12821  dvdsnegb  12822  dvdsmul1  12826  odd2np1  12863  divalglem8  12875  ndvdsadd  12883  dvdssqim  13008  nn0seqcvgd  13016  seq1st  13017  algcvgblem  13023  pythagtriplem1  13145  pythagtriplem4  13148  pythagtriplem8  13152  pythagtriplem9  13153  pythagtriplem12  13155  pythagtriplem14  13157  pythagtriplem16  13159  pcexp  13188  pc2dvds  13207  pcz  13209  fldivp1  13221  pcfac  13223  pockthg  13229  infpnlem1  13233  prmreclem1  13239  prmreclem2  13240  1arith  13250  4sqlem11  13278  vdwlem2  13305  vdwlem8  13311  vdwnnlem2  13319  pwsval  13663  isacs1i  13837  ismgmid  14665  mhmpropd  14699  grpsubid1  14829  mulgnnp1  14853  mulgsubcl  14859  mulgnn0z  14865  mulgnndir  14867  mulgneg2  14872  lagsubg  14957  ghmco  14980  pgpfi2  15195  efgsfo  15326  frgpupf  15360  frgpup1  15362  ablfac1eu  15586  pgpfac1lem2  15588  ablfaclem3  15600  dvdsrid  15711  dvdsrneg  15714  dvr1  15749  abv1  15876  lbsexg  16191  xrsds  16696  znf1o  16787  isclo  17106  resttopon  17179  restcld  17190  restcls  17199  iscn  17253  iscnp  17255  cnco  17284  cndis  17309  cnindis  17310  cmpsub  17417  hauscmplem  17423  cmpfii  17426  ptcnplem  17606  txtube  17625  txcmplem1  17626  xkoptsub  17639  qtoptop  17685  kqfval  17708  hmeoco  17757  fileln0  17835  trfil1  17871  trfil2  17872  trufil  17895  elfm3  17935  hausflf2  17983  isucn  18261  bl2in  18383  metss2lem  18494  metss2  18495  stdbdxmet  18498  metrest  18507  nmfval2  18591  nmval2  18592  nmoix  18716  ioo2bl  18777  xrsxmet  18793  expcn  18855  elcncf  18872  icccvx  18928  iscmet3  19199  causs  19204  metcld2  19212  cmetss  19220  cncmet  19228  bcth3  19237  ovolgelb  19329  ovolfi  19343  shft2rab  19357  uniioombllem3  19430  dyadmax  19443  dyadmbl  19445  subopnmbl  19449  volcn  19451  mbfid  19481  mbfeqalem  19487  mbfres  19489  cnmbf  19504  i1fmulc  19548  mbfi1fseqlem3  19562  mbfi1fseqlem4  19563  itg2seq  19587  itg2gt0  19605  itgss3  19659  dvexp  19792  plypow  20077  plyeq0lem  20082  coeidlem  20109  dgrlt  20137  dgrcolem2  20145  elqaalem2  20190  aacjcl  20197  aaliou3lem1  20212  aaliou3lem2  20213  pserdvlem2  20297  abelthlem8  20308  cosord  20387  sinord  20389  resinf1o  20391  relogexp  20443  logdivlt  20469  advlogexp  20499  logcxp  20513  cxpcl  20518  rpcxpcl  20520  cxpne0  20521  birthdaylem2  20744  cxplim  20763  divsqrsumo1  20775  wilthlem1  20804  ftalem7  20814  basellem1  20816  sgmss  20842  issqf  20872  sqf11  20875  sgmf  20881  sgmnncl  20883  sqff1o  20918  dvdsflsumcom  20926  dvdsmulf1o  20932  sgmppw  20934  chtublem  20948  chtub  20949  logexprlim  20962  bposlem3  21023  bposlem5  21025  bposlem6  21026  lgsdirnn0  21076  lgsquad2  21097  lgsquad3  21098  dchrisumlem1  21136  dchrisumlem2  21137  dchrisumlem3  21138  mulogsumlem  21178  usgrafilem2  21379  cusgraexi  21430  cusgrafilem2  21442  hashnbgravdg  21635  nvo00  22215  nmorepnf  22222  ubthlem1  22325  normpyc  22601  occon3  22752  pjpreeq  22853  idcnop  23437  riesz3i  23518  cnlnssadj  23536  rnbra  23563  strlem3a  23708  cvcon3  23740  ssdmd1  23769  ssdmd2  23770  fzsplit3  24103  ishashinf  24112  esumcst  24408  dmvlsiga  24465  ballotlemimin  24716  zetacvg  24752  derangsn  24809  iscvm  24899  cvmsval  24906  cvmliftlem7  24931  cvmlift2lem12  24954  supfz  25152  zprod  25216  faclimlem3  25312  preduz  25414  predfz  25417  wfrlem10  25479  nobndlem2  25561  brbtwn  25742  bpolylem  25998  bpolysum  26003  bpolydiflem  26004  fsumkthpow  26006  nndivlub  26112  ltflcei  26140  lxflflp1  26142  mblfinlem  26143  mblfinlem2  26144  mblfinlem3  26145  opnrebl2  26214  nn0prpwlem  26215  tailval  26292  fzadd2  26335  caushft  26357  ismtyval  26399  heiborlem7  26416  heiborlem10  26419  heibor  26420  elrfirn  26639  ismrc  26645  nacsfix  26656  mzpcompact2lem  26698  eldiophb  26705  ellz1  26715  rexrabdioph  26744  rpexpmord  26901  congrep  26928  jm2.26a  26961  lindfmm  27165  rngunsnply  27246  mendrng  27368  expgrowthi  27418  cnfex  27566  itgsinexp  27616  ltsubnn0  27973  ubmelm1fzo  27987  ssfzo12  27990  swrdltnd  28000  swrdnd  28001  swrdswrd  28011  swrdccatin12lem3a  28021  swrdccatin12lem3b  28022  swrdccatin12lem3  28024  swrdccat3  28029  usgra2wlkspthlem2  28037  4cycl2v2nb  28120  frg2woteqm  28162  2spotmdisj  28171  bnj545  28972  bnj929  29013  bnj953  29016

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 178  df-an 361