Theorem syl2anr 478

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 477	. 2 |- ( ( ph /\ ta ) -> th )
5	4	ancoms 453	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  4760  funco  5565  resdif  5770  fvcofneq  5961  fnprb  6046  fnprOLD  6047  fnsuppresOLD  6048  isotr  6137  weisoeq  6156  brrpssg  6473  findsg  6614  coexg  6639  xpexgALT  6681  fnsuppres  6827  oaass  7111  oeword  7140  oeworde  7143  ixpssmapg  7404  pw2f1olem  7526  domsdomtr  7557  xpen  7585  mapen  7586  mapdom1  7587  mapfienlem1  7766  elfir  7777  wdomen2  7904  carden2b  8249  harcard  8260  isinffi  8274  acnlem  8330  acndom  8333  alephdom  8363  fin23lem21  8620  fin23lem39  8631  isf32lem5  8638  fin1a2lem12  8692  ttukeylem1  8790  pwcfsdom  8859  canthp1  8933  nqereu  9210  addpqf  9225  axmulf  9425  axmulass  9436  axdistr  9437  negeu  9712  fimaxre3  10391  nnsub  10472  nn0sub  10742  elz2  10775  uzaddcl  11023  qaddcl  11081  xltneg  11299  xleneg  11300  supxrbnd1  11396  infmxrgelb  11409  iccneg  11524  uzsubsubfz  11589  fzsplit2  11592  fz0fzdiffz0  11607  fzss1  11615  uzsplit  11648  fzm1  11658  fzonlt0  11690  fzouzsplit  11702  elfzodifsumelfzo  11722  ssfzo12  11738  elfznelfzob  11749  fllt  11774  uzsup  11820  modifeq2int  11879  om2uzlt2i  11892  nn0ennn  11919  seqfveq2  11946  sermono  11956  seqf1o  11965  ser1const  11980  faclbnd  12184  bcval4  12201  bcpasc  12215  hashkf  12223  hashunx  12268  hash2prd  12300  hashfacen  12326  fz1isolem  12333  seqcoll  12335  swrdlend  12444  swrdnd  12445  swrdvalodm2  12452  swrdswrd  12473  swrdccatin12lem2  12499  swrdccat3  12502  revccat  12525  repswswrd  12541  cshwmodn  12551  cshwidxmod  12559  repswcshw  12565  2cshwid  12567  2cshwcom  12569  s1co  12580  cshco  12583  shftfval  12678  seqshft  12693  crim  12723  caubnd  12965  isercolllem2  13262  fsumcvg  13308  fsumcvg2  13323  fsumshftm  13367  fsumo1  13394  isumshft  13421  harmonic  13440  cvgrat  13462  mertenslem1  13463  rpnnen2  13627  dvdsval3  13658  negdvdsb  13668  dvdsnegb  13669  dvdsmul1  13673  odd2np1  13711  divalglem8  13723  ndvdsadd  13731  dvdssqim  13856  nn0seqcvgd  13864  seq1st  13865  algcvgblem  13871  modprm0  13992  modprmn0modprm0  13994  pythagtriplem1  14002  pythagtriplem4  14005  pythagtriplem8  14009  pythagtriplem9  14010  pythagtriplem12  14012  pythagtriplem14  14014  pythagtriplem16  14016  pcexp  14045  pc2dvds  14064  pcz  14066  fldivp1  14078  pcfac  14080  pockthg  14086  infpnlem1  14090  prmreclem1  14096  prmreclem2  14097  1arith  14107  4sqlem11  14135  vdwlem2  14162  vdwlem8  14168  vdwnnlem2  14176  cshwshashlem2  14242  cshwshashlem3  14243  pwsval  14544  isacs1i  14715  ismgmid  15555  mhmpropd  15590  grpsubid1  15731  mulgnnp1  15755  mulgsubcl  15761  mulgnn0z  15767  mulgnndir  15769  mulgneg2  15774  lagsubg  15863  ghmco  15886  symg2bas  16023  symgextfv  16043  pgpfi2  16227  efgsfo  16358  frgpupf  16392  frgpup1  16394  gsummptshft  16552  ablfac1eu  16697  pgpfac1lem2  16699  ablfaclem3  16711  dvdsrid  16867  dvdsrneg  16870  dvr1  16905  abv1  17042  lbsexg  17369  xrsds  17982  znf1o  18110  lindfmm  18382  matecl  18452  mavmul0g  18492  gsummatr01  18598  isclo  18824  resttopon  18898  restcld  18909  restcls  18918  iscn  18972  iscnp  18974  cnco  19003  cndis  19028  cnindis  19029  cmpsub  19136  hauscmplem  19142  cmpfii  19145  ptcnplem  19327  txtube  19346  txcmplem1  19347  xkoptsub  19360  qtoptop  19406  kqfval  19429  hmeoco  19478  fileln0  19556  trfil1  19592  trfil2  19593  trufil  19616  elfm3  19656  hausflf2  19704  isucn  19986  bl2in  20108  metss2lem  20219  metss2  20220  stdbdxmet  20223  metrest  20232  nmfval2  20316  nmval2  20317  nmoix  20441  ioo2bl  20503  xrsxmet  20519  expcn  20581  elcncf  20598  icccvx  20655  iscmet3  20937  causs  20942  metcld2  20950  cmetss  20958  cncmet  20966  bcth3  20975  ovolgelb  21096  ovolfi  21110  shft2rab  21124  uniioombllem3  21199  dyadmax  21212  dyadmbl  21214  subopnmbl  21218  volcn  21220  mbfid  21248  mbfeqalem  21254  mbfres  21256  cnmbf  21271  i1fmulc  21315  mbfi1fseqlem3  21329  mbfi1fseqlem4  21330  itg2seq  21354  itg2gt0  21372  itgss3  21426  dvexp  21561  plypow  21807  plyeq0lem  21812  coeidlem  21839  dgrlt  21867  dgrcolem2  21875  elqaalem2  21920  aacjcl  21927  aaliou3lem1  21942  aaliou3lem2  21943  pserdvlem2  22027  abelthlem8  22038  cosord  22122  sinord  22124  resinf1o  22126  relogexp  22178  logdivlt  22204  advlogexp  22234  logcxp  22248  cxpcl  22253  rpcxpcl  22255  cxpne0  22256  birthdaylem2  22480  cxplim  22499  divsqrsumo1  22511  wilthlem1  22540  ftalem7  22550  basellem1  22552  sgmss  22578  issqf  22608  sqf11  22611  sgmf  22617  sgmnncl  22619  sqff1o  22654  dvdsflsumcom  22662  dvdsmulf1o  22668  sgmppw  22670  chtublem  22684  chtub  22685  logexprlim  22698  bposlem3  22759  bposlem5  22761  bposlem6  22762  lgsdirnn0  22812  lgsquad2  22833  lgsquad3  22834  dchrisumlem1  22872  dchrisumlem2  22873  dchrisumlem3  22874  mulogsumlem  22914  brbtwn  23298  usgrafilem2  23478  cusgraexi  23529  cusgrafilem2  23541  hashnbgravdg  23734  nvo00  24314  nmorepnf  24321  ubthlem1  24424  normpyc  24701  occon3  24853  pjpreeq  24954  idcnop  25538  riesz3i  25619  cnlnssadj  25637  rnbra  25664  strlem3a  25809  cvcon3  25841  ssdmd1  25870  ssdmd2  25871  fzsplit3  26224  ishashinf  26231  esumcst  26660  dmvlsiga  26718  ballotlemimin  27033  zetacvg  27146  derangsn  27203  iscvm  27293  cvmsval  27300  cvmliftlem7  27325  cvmlift2lem12  27348  supfz  27531  zprod  27595  faclimlem3  27696  preduz  27806  predfz  27809  wfrlem10  27878  nobndlem2  27979  bpolylem  28336  bpolysum  28341  bpolydiflem  28342  fsumkthpow  28344  nndivlub  28449  finixpnum  28563  ltflcei  28568  lxflflp1  28570  mblfinlem2  28578  mblfinlem3  28579  mblfinlem4  28580  ftc1anclem1  28616  ftc1anclem4  28619  ftc1anclem5  28620  ftc1anclem7  28622  ftc1anclem8  28623  ftc1anc  28624  opnrebl2  28665  nn0prpwlem  28666  tailval  28743  fzadd2  28786  caushft  28806  ismtyval  28848  heiborlem7  28865  heiborlem10  28868  heibor  28869  elrfirn  29180  ismrc  29186  nacsfix  29197  mzpcompact2lem  29237  eldiophb  29244  ellz1  29254  rexrabdioph  29281  rpexpmord  29438  congrep  29465  jm2.26a  29498  rngunsnply  29679  mendrng  29698  iocmbl  29737  expgrowthi  29756  cnfex  29899  itgsinexp  29944  ltsubnn0  30331  subsubelfzo0  30359  eluzgtdifelfzo  30368  powm2modprm  30397  usgra2wlkspthlem2  30446  vfwlkniswwlkn  30489  clwlkisclwwlklem2fv2  30594  zm1nn  30617  erclwwlksym0  30627  erclwwlktr0  30628  difelfzle  30636  difelfznle  30637  cshwlemma1  30638  nbhashuvtx1  30682  rusgranumwlk  30724  4cycl2v2nb  30757  frg2woteqm  30801  2spotmdisj  30810  extwwlkfablem1  30816  numclwwlk8  30857  suppssfz  30935  telescfzgsumlem  30962  telescgsum  30967  gsummoncoe1  30997  lincresunit3  31148  lincreslvec3  31149  isldepslvec2  31152  mp2pm2mplem4  31297  chfacfisf  31341  chfacfisfcpmat  31342  chfacfpmmulgsum2  31352  cpmadugsumlemF  31363  bnj545  32221  bnj929  32262  bnj953  32265