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  4646  funco  5451  resdif  5656  fvcofneq  5846  fnprb  5931  fnprOLD  5932  fnsuppresOLD  5933  isotr  6022  weisoeq  6041  brrpssg  6357  findsg  6498  coexg  6523  xpexgALT  6565  fnsuppres  6711  oaass  6992  oeword  7021  oeworde  7024  ixpssmapg  7285  pw2f1olem  7407  domsdomtr  7438  xpen  7466  mapen  7467  mapdom1  7468  mapfienlem1  7646  elfir  7657  wdomen2  7784  carden2b  8129  harcard  8140  isinffi  8154  acnlem  8210  acndom  8213  alephdom  8243  fin23lem21  8500  fin23lem39  8511  isf32lem5  8518  fin1a2lem12  8572  ttukeylem1  8670  pwcfsdom  8739  canthp1  8813  nqereu  9090  addpqf  9105  axmulf  9305  axmulass  9316  axdistr  9317  negeu  9592  fimaxre3  10271  nnsub  10352  nn0sub  10622  elz2  10655  uzaddcl  10903  qaddcl  10961  xltneg  11179  xleneg  11180  supxrbnd1  11276  infmxrgelb  11289  iccneg  11398  uzsubsubfz  11463  fzsplit2  11466  fz0fzdiffz0  11481  fzss1  11489  uzsplit  11522  fzm1  11532  fzonlt0  11564  fzouzsplit  11576  elfzodifsumelfzo  11596  ssfzo12  11612  elfznelfzob  11623  fllt  11648  uzsup  11694  modifeq2int  11753  om2uzlt2i  11766  nn0ennn  11793  seqfveq2  11820  sermono  11830  seqf1o  11839  ser1const  11854  faclbnd  12058  bcval4  12075  bcpasc  12089  hashkf  12097  hashunx  12141  hash2prd  12173  hashfacen  12199  fz1isolem  12206  seqcoll  12208  swrdlend  12317  swrdnd  12318  swrdvalodm2  12325  swrdswrd  12346  swrdccatin12lem2  12372  swrdccat3  12375  revccat  12398  repswswrd  12414  cshwmodn  12424  cshwidxmod  12432  repswcshw  12438  2cshwid  12440  2cshwcom  12442  s1co  12453  cshco  12456  shftfval  12551  seqshft  12566  crim  12596  caubnd  12838  isercolllem2  13135  fsumcvg  13181  fsumcvg2  13196  fsumshftm  13240  fsumo1  13267  isumshft  13294  harmonic  13313  cvgrat  13335  mertenslem1  13336  rpnnen2  13500  dvdsval3  13531  negdvdsb  13541  dvdsnegb  13542  dvdsmul1  13546  odd2np1  13584  divalglem8  13596  ndvdsadd  13604  dvdssqim  13729  nn0seqcvgd  13737  seq1st  13738  algcvgblem  13744  modprm0  13865  modprmn0modprm0  13867  pythagtriplem1  13875  pythagtriplem4  13878  pythagtriplem8  13882  pythagtriplem9  13883  pythagtriplem12  13885  pythagtriplem14  13887  pythagtriplem16  13889  pcexp  13918  pc2dvds  13937  pcz  13939  fldivp1  13951  pcfac  13953  pockthg  13959  infpnlem1  13963  prmreclem1  13969  prmreclem2  13970  1arith  13980  4sqlem11  14008  vdwlem2  14035  vdwlem8  14041  vdwnnlem2  14049  cshwshashlem2  14115  cshwshashlem3  14116  pwsval  14416  isacs1i  14587  ismgmid  15427  mhmpropd  15462  grpsubid1  15602  mulgnnp1  15626  mulgsubcl  15632  mulgnn0z  15638  mulgnndir  15640  mulgneg2  15645  lagsubg  15734  ghmco  15757  symg2bas  15894  symgextfv  15914  pgpfi2  16096  efgsfo  16227  frgpupf  16261  frgpup1  16263  gsummptshft  16419  ablfac1eu  16562  pgpfac1lem2  16564  ablfaclem3  16576  dvdsrid  16731  dvdsrneg  16734  dvr1  16769  abv1  16896  lbsexg  17222  xrsds  17831  znf1o  17959  lindfmm  18231  matecl  18301  mavmul0g  18339  gsummatr01  18440  isclo  18666  resttopon  18740  restcld  18751  restcls  18760  iscn  18814  iscnp  18816  cnco  18845  cndis  18870  cnindis  18871  cmpsub  18978  hauscmplem  18984  cmpfii  18987  ptcnplem  19169  txtube  19188  txcmplem1  19189  xkoptsub  19202  qtoptop  19248  kqfval  19271  hmeoco  19320  fileln0  19398  trfil1  19434  trfil2  19435  trufil  19458  elfm3  19498  hausflf2  19546  isucn  19828  bl2in  19950  metss2lem  20061  metss2  20062  stdbdxmet  20065  metrest  20074  nmfval2  20158  nmval2  20159  nmoix  20283  ioo2bl  20345  xrsxmet  20361  expcn  20423  elcncf  20440  icccvx  20497  iscmet3  20779  causs  20784  metcld2  20792  cmetss  20800  cncmet  20808  bcth3  20817  ovolgelb  20938  ovolfi  20952  shft2rab  20966  uniioombllem3  21040  dyadmax  21053  dyadmbl  21055  subopnmbl  21059  volcn  21061  mbfid  21089  mbfeqalem  21095  mbfres  21097  cnmbf  21112  i1fmulc  21156  mbfi1fseqlem3  21170  mbfi1fseqlem4  21171  itg2seq  21195  itg2gt0  21213  itgss3  21267  dvexp  21402  plypow  21648  plyeq0lem  21653  coeidlem  21680  dgrlt  21708  dgrcolem2  21716  elqaalem2  21761  aacjcl  21768  aaliou3lem1  21783  aaliou3lem2  21784  pserdvlem2  21868  abelthlem8  21879  cosord  21963  sinord  21965  resinf1o  21967  relogexp  22019  logdivlt  22045  advlogexp  22075  logcxp  22089  cxpcl  22094  rpcxpcl  22096  cxpne0  22097  birthdaylem2  22321  cxplim  22340  divsqrsumo1  22352  wilthlem1  22381  ftalem7  22391  basellem1  22393  sgmss  22419  issqf  22449  sqf11  22452  sgmf  22458  sgmnncl  22460  sqff1o  22495  dvdsflsumcom  22503  dvdsmulf1o  22509  sgmppw  22511  chtublem  22525  chtub  22526  logexprlim  22539  bposlem3  22600  bposlem5  22602  bposlem6  22603  lgsdirnn0  22653  lgsquad2  22674  lgsquad3  22675  dchrisumlem1  22713  dchrisumlem2  22714  dchrisumlem3  22715  mulogsumlem  22755  brbtwn  23096  usgrafilem2  23276  cusgraexi  23327  cusgrafilem2  23339  hashnbgravdg  23532  nvo00  24112  nmorepnf  24119  ubthlem1  24222  normpyc  24499  occon3  24651  pjpreeq  24752  idcnop  25336  riesz3i  25417  cnlnssadj  25435  rnbra  25462  strlem3a  25607  cvcon3  25639  ssdmd1  25668  ssdmd2  25669  fzsplit3  26029  ishashinf  26036  esumcst  26466  dmvlsiga  26524  ballotlemimin  26840  zetacvg  26953  derangsn  27010  iscvm  27100  cvmsval  27107  cvmliftlem7  27132  cvmlift2lem12  27155  supfz  27337  zprod  27401  faclimlem3  27502  preduz  27612  predfz  27615  wfrlem10  27684  nobndlem2  27785  bpolylem  28142  bpolysum  28147  bpolydiflem  28148  fsumkthpow  28150  nndivlub  28256  finixpnum  28367  ltflcei  28372  lxflflp1  28374  mblfinlem2  28382  mblfinlem3  28383  mblfinlem4  28384  ftc1anclem1  28420  ftc1anclem4  28423  ftc1anclem5  28424  ftc1anclem7  28426  ftc1anclem8  28427  ftc1anc  28428  opnrebl2  28469  nn0prpwlem  28470  tailval  28547  fzadd2  28590  caushft  28610  ismtyval  28652  heiborlem7  28669  heiborlem10  28672  heibor  28673  elrfirn  28984  ismrc  28990  nacsfix  29001  mzpcompact2lem  29041  eldiophb  29048  ellz1  29058  rexrabdioph  29085  rpexpmord  29242  congrep  29269  jm2.26a  29302  rngunsnply  29483  mendrng  29502  iocmbl  29541  expgrowthi  29560  cnfex  29703  itgsinexp  29748  ltsubnn0  30135  subsubelfzo0  30163  eluzgtdifelfzo  30172  powm2modprm  30201  usgra2wlkspthlem2  30250  vfwlkniswwlkn  30293  clwlkisclwwlklem2fv2  30398  zm1nn  30421  erclwwlksym0  30431  erclwwlktr0  30432  difelfzle  30440  difelfznle  30441  cshwlemma1  30442  nbhashuvtx1  30486  rusgranumwlk  30528  4cycl2v2nb  30561  frg2woteqm  30605  2spotmdisj  30614  extwwlkfablem1  30620  numclwwlk8  30661  lincresunit3  30904  lincreslvec3  30905  isldepslvec2  30908  bnj545  31775  bnj929  31816  bnj953  31819