Theorem syl2anr 475

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

Syntax hints:   -> wi 4   /\ wa 369

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 185  df-an 371

This theorem is referenced by:  swopo  4638  funco  5444  resdif  5649  fvcofneq  5839  fnprb  5923  fnprOLD  5924  fnsuppresOLD  5925  isotr  6014  weisoeq  6033  brrpssg  6351  findsg  6492  coexg  6517  xpexgALT  6559  fnsuppres  6705  oaass  6988  oeword  7017  oeworde  7020  ixpssmapg  7281  pw2f1olem  7403  domsdomtr  7434  xpen  7462  mapen  7463  mapdom1  7464  mapfienlem1  7642  elfir  7653  wdomen2  7780  carden2b  8125  harcard  8136  isinffi  8150  acnlem  8206  acndom  8209  alephdom  8239  fin23lem21  8496  fin23lem39  8507  isf32lem5  8514  fin1a2lem12  8568  ttukeylem1  8666  pwcfsdom  8735  canthp1  8809  nqereu  9086  addpqf  9101  axmulf  9301  axmulass  9312  axdistr  9313  negeu  9588  fimaxre3  10267  nnsub  10348  nn0sub  10618  elz2  10651  uzaddcl  10899  qaddcl  10957  xltneg  11175  xleneg  11176  supxrbnd1  11272  infmxrgelb  11285  iccneg  11393  uzsubsubfz  11458  fzsplit2  11461  fz0fzdiffz0  11476  fzss1  11484  uzsplit  11514  fzm1  11524  fzonlt0  11556  fzouzsplit  11568  elfzodifsumelfzo  11588  ssfzo12  11604  elfznelfzob  11615  fllt  11640  uzsup  11686  modifeq2int  11745  om2uzlt2i  11758  nn0ennn  11785  seqfveq2  11812  sermono  11822  seqf1o  11831  ser1const  11846  faclbnd  12050  bcval4  12067  bcpasc  12081  hashkf  12089  hashunx  12133  hash2prd  12165  hashfacen  12191  fz1isolem  12198  seqcoll  12200  swrdlend  12309  swrdnd  12310  swrdvalodm2  12317  swrdswrd  12338  swrdccatin12lem2  12364  swrdccat3  12367  revccat  12390  repswswrd  12406  cshwmodn  12416  cshwidxmod  12424  repswcshw  12430  2cshwid  12432  2cshwcom  12434  s1co  12445  cshco  12448  shftfval  12543  seqshft  12558  crim  12588  caubnd  12830  isercolllem2  13127  fsumcvg  13173  fsumcvg2  13188  fsumshftm  13231  fsumo1  13258  isumshft  13285  harmonic  13304  cvgrat  13326  mertenslem1  13327  rpnnen2  13491  dvdsval3  13522  negdvdsb  13532  dvdsnegb  13533  dvdsmul1  13537  odd2np1  13575  divalglem8  13587  ndvdsadd  13595  dvdssqim  13720  nn0seqcvgd  13728  seq1st  13729  algcvgblem  13735  modprm0  13856  modprmn0modprm0  13858  pythagtriplem1  13866  pythagtriplem4  13869  pythagtriplem8  13873  pythagtriplem9  13874  pythagtriplem12  13876  pythagtriplem14  13878  pythagtriplem16  13880  pcexp  13909  pc2dvds  13928  pcz  13930  fldivp1  13942  pcfac  13944  pockthg  13950  infpnlem1  13954  prmreclem1  13960  prmreclem2  13961  1arith  13971  4sqlem11  13999  vdwlem2  14026  vdwlem8  14032  vdwnnlem2  14040  cshwshashlem2  14106  cshwshashlem3  14107  pwsval  14407  isacs1i  14578  ismgmid  15418  mhmpropd  15453  grpsubid1  15591  mulgnnp1  15615  mulgsubcl  15621  mulgnn0z  15627  mulgnndir  15629  mulgneg2  15634  lagsubg  15723  ghmco  15746  symg2bas  15883  symgextfv  15903  pgpfi2  16085  efgsfo  16216  frgpupf  16250  frgpup1  16252  ablfac1eu  16548  pgpfac1lem2  16550  ablfaclem3  16562  dvdsrid  16677  dvdsrneg  16680  dvr1  16715  abv1  16842  lbsexg  17167  xrsds  17700  znf1o  17826  lindfmm  18098  matecl  18168  mavmul0g  18206  gsummatr01  18307  isclo  18533  resttopon  18607  restcld  18618  restcls  18627  iscn  18681  iscnp  18683  cnco  18712  cndis  18737  cnindis  18738  cmpsub  18845  hauscmplem  18851  cmpfii  18854  ptcnplem  19036  txtube  19055  txcmplem1  19056  xkoptsub  19069  qtoptop  19115  kqfval  19138  hmeoco  19187  fileln0  19265  trfil1  19301  trfil2  19302  trufil  19325  elfm3  19365  hausflf2  19413  isucn  19695  bl2in  19817  metss2lem  19928  metss2  19929  stdbdxmet  19932  metrest  19941  nmfval2  20025  nmval2  20026  nmoix  20150  ioo2bl  20212  xrsxmet  20228  expcn  20290  elcncf  20307  icccvx  20364  iscmet3  20646  causs  20651  metcld2  20659  cmetss  20667  cncmet  20675  bcth3  20684  ovolgelb  20805  ovolfi  20819  shft2rab  20833  uniioombllem3  20907  dyadmax  20920  dyadmbl  20922  subopnmbl  20926  volcn  20928  mbfid  20956  mbfeqalem  20962  mbfres  20964  cnmbf  20979  i1fmulc  21023  mbfi1fseqlem3  21037  mbfi1fseqlem4  21038  itg2seq  21062  itg2gt0  21080  itgss3  21134  dvexp  21269  plypow  21558  plyeq0lem  21563  coeidlem  21590  dgrlt  21618  dgrcolem2  21626  elqaalem2  21671  aacjcl  21678  aaliou3lem1  21693  aaliou3lem2  21694  pserdvlem2  21778  abelthlem8  21789  cosord  21873  sinord  21875  resinf1o  21877  relogexp  21929  logdivlt  21955  advlogexp  21985  logcxp  21999  cxpcl  22004  rpcxpcl  22006  cxpne0  22007  birthdaylem2  22231  cxplim  22250  divsqrsumo1  22262  wilthlem1  22291  ftalem7  22301  basellem1  22303  sgmss  22329  issqf  22359  sqf11  22362  sgmf  22368  sgmnncl  22370  sqff1o  22405  dvdsflsumcom  22413  dvdsmulf1o  22419  sgmppw  22421  chtublem  22435  chtub  22436  logexprlim  22449  bposlem3  22510  bposlem5  22512  bposlem6  22513  lgsdirnn0  22563  lgsquad2  22584  lgsquad3  22585  dchrisumlem1  22623  dchrisumlem2  22624  dchrisumlem3  22625  mulogsumlem  22665  brbtwn  22968  usgrafilem2  23148  cusgraexi  23199  cusgrafilem2  23211  hashnbgravdg  23404  nvo00  23984  nmorepnf  23991  ubthlem1  24094  normpyc  24371  occon3  24523  pjpreeq  24624  idcnop  25208  riesz3i  25289  cnlnssadj  25307  rnbra  25334  strlem3a  25479  cvcon3  25511  ssdmd1  25540  ssdmd2  25541  fzsplit3  25901  ishashinf  25908  esumcst  26368  dmvlsiga  26426  ballotlemimin  26736  zetacvg  26849  derangsn  26906  iscvm  26996  cvmsval  27003  cvmliftlem7  27028  cvmlift2lem12  27051  supfz  27233  zprod  27297  faclimlem3  27398  preduz  27508  predfz  27511  wfrlem10  27580  nobndlem2  27681  bpolylem  28038  bpolysum  28043  bpolydiflem  28044  fsumkthpow  28046  nndivlub  28152  finixpnum  28258  ltflcei  28263  lxflflp1  28265  mblfinlem2  28273  mblfinlem3  28274  mblfinlem4  28275  ftc1anclem1  28311  ftc1anclem4  28314  ftc1anclem5  28315  ftc1anclem7  28317  ftc1anclem8  28318  ftc1anc  28319  opnrebl2  28360  nn0prpwlem  28361  tailval  28438  fzadd2  28481  caushft  28501  ismtyval  28543  heiborlem7  28560  heiborlem10  28563  heibor  28564  elrfirn  28876  ismrc  28882  nacsfix  28893  mzpcompact2lem  28933  eldiophb  28940  ellz1  28950  rexrabdioph  28977  rpexpmord  29134  congrep  29161  jm2.26a  29194  rngunsnply  29375  mendrng  29394  iocmbl  29433  expgrowthi  29452  cnfex  29595  itgsinexp  29641  ltsubnn0  30028  subsubelfzo0  30056  eluzgtdifelfzo  30065  powm2modprm  30094  usgra2wlkspthlem2  30143  vfwlkniswwlkn  30186  clwlkisclwwlklem2fv2  30291  zm1nn  30314  erclwwlksym0  30324  erclwwlktr0  30325  difelfzle  30333  difelfznle  30334  cshwlemma1  30335  nbhashuvtx1  30379  rusgranumwlk  30421  4cycl2v2nb  30454  frg2woteqm  30498  2spotmdisj  30507  extwwlkfablem1  30513  numclwwlk8  30554  lincresunit3  30724  lincreslvec3  30725  isldepslvec2  30728  bnj545  31590  bnj929  31631  bnj953  31634