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  4810  funco  5624  resdif  5834  fvcofneq  6027  fnprb  6117  fnprOLD  6118  fnsuppresOLD  6119  isotr  6218  weisoeq  6237  brrpssg  6564  findsg  6705  coexg  6732  xpexgALT  6774  fnsuppres  6924  oaass  7207  oeword  7236  oeworde  7239  ixpssmapg  7496  pw2f1olem  7618  domsdomtr  7649  xpen  7677  mapen  7678  mapdom1  7679  mapfienlem1  7860  elfir  7871  wdomen2  7999  carden2b  8344  harcard  8355  isinffi  8369  acnlem  8425  acndom  8428  alephdom  8458  fin23lem21  8715  fin23lem39  8726  isf32lem5  8733  fin1a2lem12  8787  ttukeylem1  8885  pwcfsdom  8954  canthp1  9028  nqereu  9303  addpqf  9318  axmulf  9519  axmulass  9530  axdistr  9531  negeu  9806  fimaxre3  10488  nnsub  10570  nn0sub  10842  elz2  10877  uzaddcl  11133  qaddcl  11194  xltneg  11412  xleneg  11413  supxrbnd1  11509  infmxrgelb  11522  iccneg  11637  uzsubsubfz  11703  fzsplit2  11706  fzss1  11718  uzsplit  11746  fzm1  11754  fz0fzdiffz0  11777  difelfzle  11781  difelfznle  11782  fzonlt0  11812  fzouzsplit  11824  eluzgtdifelfzo  11842  elfzodifsumelfzo  11846  ssfzo12  11869  elfznelfzob  11880  fllt  11907  uzsup  11953  modifeq2int  12012  om2uzlt2i  12025  nn0ennn  12052  suppssfz  12063  seqfveq2  12092  sermono  12102  seqf1o  12111  ser1const  12126  faclbnd  12330  bcval4  12347  bcpasc  12361  hashkf  12369  hashunx  12416  hashfacen  12463  fz1isolem  12470  seqcoll  12472  hash2prd  12478  swrdlend  12613  swrdnd  12614  swrdvalodm2  12621  swrdswrd  12642  swrdccatin12lem2  12671  swrdccat3  12674  revccat  12697  repswswrd  12713  cshwmodn  12723  cshwidxmod  12731  repswcshw  12737  2cshwid  12739  2cshwcom  12741  2cshwcshw  12750  cshwcshid  12752  cshwcsh2id  12753  s1co  12756  cshco  12759  shftfval  12860  seqshft  12875  crim  12905  caubnd  13147  isercolllem2  13444  fsumcvg  13490  fsumcvg2  13505  fsumshftm  13552  fsumo1  13582  isumshft  13607  harmonic  13626  cvgrat  13648  mertenslem1  13649  rpnnen2  13813  dvdsval3  13844  negdvdsb  13854  dvdsnegb  13855  dvdsmul1  13859  odd2np1  13898  divalglem8  13910  ndvdsadd  13918  dvdssqim  14043  nn0seqcvgd  14051  seq1st  14052  algcvgblem  14058  powm2modprm  14180  modprm0  14182  modprmn0modprm0  14184  pythagtriplem1  14192  pythagtriplem4  14195  pythagtriplem8  14199  pythagtriplem9  14200  pythagtriplem12  14202  pythagtriplem14  14204  pythagtriplem16  14206  pcexp  14235  pc2dvds  14254  pcz  14256  fldivp1  14268  pcfac  14270  pockthg  14276  infpnlem1  14280  prmreclem1  14286  prmreclem2  14287  1arith  14297  4sqlem11  14325  vdwlem2  14352  vdwlem8  14358  vdwnnlem2  14366  cshwshashlem2  14432  cshwshashlem3  14433  pwsval  14734  isacs1i  14905  ismgmid  15745  mhmpropd  15780  grpsubid1  15921  mulgnnp1  15947  mulgsubcl  15953  mulgnn0z  15959  mulgnndir  15961  mulgneg2  15966  lagsubg  16055  ghmco  16078  symg2bas  16215  symgextfv  16235  pgpfi2  16419  efgsfo  16550  frgpupf  16584  frgpup1  16586  gsummptshft  16744  telgsumfzslem  16805  telgsums  16810  ablfac1eu  16911  pgpfac1lem2  16913  ablfaclem3  16925  dvdsrid  17081  dvdsrneg  17084  dvr1  17119  abv1  17262  lbsexg  17590  gsummoncoe1  18114  xrsds  18226  znf1o  18354  lindfmm  18626  matecl  18691  mavmul0g  18819  gsummatr01  18925  mp2pm2mplem4  19074  chfacfisf  19119  chfacfisfcpmat  19120  chfacfpmmulgsum2  19130  cpmadugsumlemF  19141  isclo  19351  resttopon  19425  restcld  19436  restcls  19445  iscn  19499  iscnp  19501  cnco  19530  cndis  19555  cnindis  19556  cmpsub  19663  hauscmplem  19669  cmpfii  19672  ptcnplem  19854  txtube  19873  txcmplem1  19874  xkoptsub  19887  qtoptop  19933  kqfval  19956  hmeoco  20005  fileln0  20083  trfil1  20119  trfil2  20120  trufil  20143  elfm3  20183  hausflf2  20231  isucn  20513  bl2in  20635  metss2lem  20746  metss2  20747  stdbdxmet  20750  metrest  20759  nmfval2  20843  nmval2  20844  nmoix  20968  ioo2bl  21030  xrsxmet  21046  expcn  21108  elcncf  21125  icccvx  21182  iscmet3  21464  causs  21469  metcld2  21477  cmetss  21485  cncmet  21493  bcth3  21502  ovolgelb  21623  ovolfi  21637  shft2rab  21651  uniioombllem3  21726  dyadmax  21739  dyadmbl  21741  subopnmbl  21745  volcn  21747  mbfid  21775  mbfeqalem  21781  mbfres  21783  cnmbf  21798  i1fmulc  21842  mbfi1fseqlem3  21856  mbfi1fseqlem4  21857  itg2seq  21881  itg2gt0  21899  itgss3  21953  dvexp  22088  plypow  22334  plyeq0lem  22339  coeidlem  22366  dgrlt  22394  dgrcolem2  22402  elqaalem2  22447  aacjcl  22454  aaliou3lem1  22469  aaliou3lem2  22470  pserdvlem2  22554  abelthlem8  22565  cosord  22649  sinord  22651  resinf1o  22653  relogexp  22705  logdivlt  22731  advlogexp  22761  logcxp  22775  cxpcl  22780  rpcxpcl  22782  cxpne0  22783  birthdaylem2  23007  cxplim  23026  divsqrtsumo1  23038  wilthlem1  23067  ftalem7  23077  basellem1  23079  sgmss  23105  issqf  23135  sqf11  23138  sgmf  23144  sgmnncl  23146  sqff1o  23181  dvdsflsumcom  23189  dvdsmulf1o  23195  sgmppw  23197  chtublem  23211  chtub  23212  logexprlim  23225  bposlem3  23286  bposlem5  23288  bposlem6  23289  lgsdirnn0  23339  lgsquad2  23360  lgsquad3  23361  dchrisumlem1  23399  dchrisumlem2  23400  dchrisumlem3  23401  mulogsumlem  23441  brbtwn  23875  usgrafilem2  24085  cusgraexi  24141  cusgrafilem2  24153  usgra2wlkspthlem2  24293  vfwlkniswwlkn  24379  clwlkisclwwlklem2fv2  24456  hashnbgravdg  24586  nbhashuvtx1  24588  rusgranumwlk  24630  4cycl2v2nb  24689  frg2woteqm  24733  2spotmdisj  24742  extwwlkfablem1  24748  numclwwlk8  24789  nvo00  25349  nmorepnf  25356  ubthlem1  25459  normpyc  25736  occon3  25888  pjpreeq  25989  idcnop  26573  riesz3i  26654  cnlnssadj  26672  rnbra  26699  strlem3a  26844  cvcon3  26876  ssdmd1  26905  ssdmd2  26906  fzsplit3  27264  ishashinf  27271  esumcst  27708  dmvlsiga  27766  ballotlemimin  28081  zetacvg  28194  derangsn  28251  iscvm  28341  cvmsval  28348  cvmliftlem7  28373  cvmlift2lem12  28396  supfz  28579  zprod  28643  faclimlem3  28744  preduz  28854  predfz  28857  wfrlem10  28926  nobndlem2  29027  bpolylem  29384  bpolysum  29389  bpolydiflem  29390  fsumkthpow  29392  nndivlub  29497  finixpnum  29612  ltflcei  29617  lxflflp1  29619  mblfinlem2  29627  mblfinlem3  29628  mblfinlem4  29629  ftc1anclem1  29665  ftc1anclem4  29668  ftc1anclem5  29669  ftc1anclem7  29671  ftc1anclem8  29672  ftc1anc  29673  opnrebl2  29714  nn0prpwlem  29715  tailval  29792  fzadd2  29835  caushft  29855  ismtyval  29897  heiborlem7  29914  heiborlem10  29917  heibor  29918  elrfirn  30229  ismrc  30235  nacsfix  30246  mzpcompact2lem  30286  eldiophb  30292  ellz1  30302  rexrabdioph  30329  rpexpmord  30486  congrep  30513  jm2.26a  30546  rngunsnply  30727  mendrng  30746  iocmbl  30785  isprm7  30795  expgrowthi  30838  cnfex  30981  itgsinexp  31272  zm1nn  31794  ltsubnn0  31796  subsubelfzo0  31807  lincresunit3  32155  lincreslvec3  32156  isldepslvec2  32159  bnj545  33032  bnj929  33073  bnj953  33076