Theorem syl2an 289

Description: A double syllogism inference. (Contributed by NM, 31-Jan-1997.)

Hypotheses

Ref	Expression
syl2an.1	|- ( ph -> ps )
syl2an.2	|- ( ta -> ch )
syl2an.3	|- ( ( ps /\ ch ) -> th )

Assertion

Ref	Expression
syl2an	|- ( ( ph /\ ta ) -> th )

Proof of Theorem syl2an

Step	Hyp	Ref	Expression
1		syl2an.2	. 2 |- ( ta -> ch )
2		syl2an.1	. . 3 |- ( ph -> ps )
3		syl2an.3	. . 3 |- ( ( ps /\ ch ) -> th )
4	2, 3	sylan 283	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2 286	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  syl2anr  290  anim12i  338  syl2an2  598  syl2an2r  599  orandc  948  mp3an3an  1380  eqeqan12d  2248  sylan9eq  2285  csbcomg  3160  sylan9ss  3250  ssconb  3351  ineqan12d  3423  dfopg  3880  breqan12d  4124  opexg  4343  copsex2g  4361  ordin  4505  onin  4506  unexg  4563  eusv1  4572  opelvvg  4798  opthprc  4800  opbrop  4828  relop  4904  dmpropg  5234  unixpm  5297  funssres  5394  funinsn  5404  funtp  5408  fnco  5465  resasplitss  5543  fodmrnu  5597  relrnfvex  5687  funopdmsn  5863  fconst2g  5898  oveqan12d  6068  ovi3  6190  ovg  6192  f1opw2  6260  off  6278  offres  6327  suppfnss  6456  iunon  6514  nnsucsssuc  6724  nnaword1  6745  ertr  6781  erex  6790  brecop  6858  ecovdi  6879  ecovidi  6880  mapvalg  6891  pmvalg  6892  pmss12g  6908  mapsn  6924  en2sn  7054  xpf1o  7096  xpen  7097  phplem4  7108  ssfilem  7129  ssfilemd  7131  diffitest  7143  en1eqsn  7217  sbthlem7  7232  fsuppxpfi  7248  ordiso  7326  updjud  7372  fodju0  7437  finnum  7478  pr2nelem  7487  djucomen  7522  exmidontriimlem1  7527  2onetap  7568  ltsopi  7634  pitric  7635  pitri3or  7636  ltdcpi  7637  mulclpi  7642  addcompig  7643  mulcompig  7645  distrpig  7647  ltexpi  7651  ltapig  7652  ltmpig  7653  dfplpq2  7668  dfmpq2  7669  enqbreq2  7671  enqdc  7675  addcmpblnq  7681  addpipqqslem  7683  mulpipq2  7685  mulpipq  7686  mulpipqqs  7687  addclnq  7689  distrnqg  7701  ltdcnq  7711  ltrnqg  7734  enq0breq  7750  addclnq0  7765  nqnq0a  7768  nqnq0m  7769  nq0m0r  7770  distrnq0  7773  mulcomnq0  7774  genipv  7823  genplt2i  7824  genpelvl  7826  genpelvu  7827  addnqprlemrl  7871  addnqprlemru  7872  addnqprlemfl  7873  addnqprlemfu  7874  addnqpr  7875  mulnqprlemrl  7887  mulnqprlemru  7888  mulnqprlemfl  7889  mulnqprlemfu  7890  mulnqpr  7891  distrlem4prl  7898  distrlem4pru  7899  ltnqpr  7907  recexprlemloc  7945  archrecnq  7977  mulclsr  8068  1idsr  8082  00sr  8083  prsradd  8100  axmulass  8187  axdistr  8188  axcnre  8195  peano5nnnn  8206  mulrid  8270  axltadd  8342  lenlt  8348  cnegexlem3  8449  cnegex  8450  resubcl  8536  subeqrev  8648  muladd  8656  mulsub  8673  mulsub2  8674  ltaddsub2  8710  leaddsub2  8712  leltadd  8720  ltaddpos2  8726  posdif  8728  addge02  8746  mullt0  8753  recexre  8851  recextlem1  8924  recexap  8926  divmuldivap  8985  conjmulap  9002  div2subap  9110  prodgt02  9126  prodge02  9128  lemul2  9130  lemul2a  9132  ltmulgt12  9138  lemulge12  9140  ltmuldiv2  9148  ltdivmul2  9151  ledivmul2  9153  lemuldiv2  9155  negiso  9228  cju  9234  peano5nni  9239  nnaddcl  9256  nnmulcl  9257  nnsub  9275  addltmul  9474  avgle1  9478  avgle2  9479  nnrecl  9493  nn0nnaddcl  9526  zsubcl  9617  zleloe  9623  znnsub  9628  nzadd  9629  zmulcl  9630  zltp1le  9631  zleltp1  9632  nnleltp1  9636  nnltp1le  9637  nnaddm1cl  9638  nn0ltp1le  9639  nn0leltp1  9640  nn0ltlem1  9641  znn0sub  9642  nn0sub  9643  elz2  9648  zapne  9651  zdcle  9653  zdclt  9654  zltlen  9655  nn0lem1lt  9660  nnlem1lt  9661  nnltlem1  9662  zdiv  9665  zextle  9668  zextlt  9669  btwnnz  9671  prime  9676  nneo  9680  peano2uz2  9684  peano5uzti  9685  uzind  9688  fzind  9692  fnn0ind  9693  uzneg  9872  uz11  9876  eluzp1m1  9877  eluzp1p1  9879  uzin  9886  indstr  9924  uz2mulcl  9939  qre  9956  qaddcl  9966  qsubcl  9969  qltlen  9971  qlttri2  9972  irradd  9977  elpqb  9981  cnref1o  9982  rpaddcl  10009  rpmulcl  10010  rpdivcl  10011  rexadd  10184  rexsub  10185  xaddcom  10193  xnn0xadd0  10199  xnegdi  10200  elicc2  10270  iccshftr  10326  iccshftl  10328  iccdil  10330  icccntr  10332  fzval2  10344  elfz1eq  10368  peano2fzr  10370  fznlem  10374  fzsplit2  10383  fzaddel  10392  fzsubel  10393  fzrev2  10418  fzrev3  10420  uzsplit  10425  fzrevral  10438  fzrevral3  10440  fzshftral  10441  elfz2nn0  10445  fznn0sub2  10461  fz0fzdiffz0  10463  elfzmlbp  10465  difelfzle  10467  difelfznle  10468  1fv  10472  elfzouz2  10495  fzo0n  10501  fzouzsplit  10514  fzoun  10516  elfzo0le  10523  fzonmapblen  10525  fzofzim  10526  fzoaddel2  10534  eluzgtdifelfzo  10541  elfzodifsumelfzo  10545  ubmelm1fzo  10570  fzofzp1b  10572  fzosplitprm1  10579  fzostep1  10582  subfzo0  10587  zsupcllemstep  10588  qdclt  10604  qbtwnxr  10616  flqbi2  10650  divfl0  10655  flqzadd  10657  flqmulnn0  10658  addmodidr  10734  modfzo0difsn  10756  frec2uzltd  10764  frec2uzrand  10766  frecfzen2  10788  seqshft2g  10843  seq3split  10849  seqsplitg  10850  seq3caopr2  10854  seqcaopr2g  10855  seqf1oglem2  10881  exp3vallem  10901  expcllem  10911  expcl2lemap  10912  1exp  10929  expge1  10937  expadd  10942  expmul  10945  expsubap  10948  leexp1a  10955  lt2sq  10974  le2sq  10975  sumsqeq0  10979  qsqeqor  11011  bernneq  11021  bernneq2  11022  sq11ap  11068  facdiv  11099  faclbnd  11102  faclbnd3  11104  faclbnd6  11105  facavg  11107  bcrpcl  11114  bccmpl  11115  fiubm  11191  seq3coll  11210  eqwrd  11261  ccatcl  11277  ccatclab  11278  ccatlen  11279  ccat0  11280  ccatval1  11281  ccatval2  11282  elfzelfzccat  11284  ccatvalfn  11285  ccatsymb  11286  ccatval21sw  11289  ccatrn  11293  lswccatn0lsw  11295  ccatalpha  11297  ccatrcl1  11298  swrdfv2  11351  swrdsbslen  11354  swrdspsleq  11355  swrdccat2  11359  pfxclz  11367  ccatpfx  11389  pfxccat1  11390  swrdswrdlem  11392  pfxswrd  11394  pfxccatin12lem4  11414  pfxccatin12lem1  11416  pfxccatin12lem2  11419  pfxccatin12lem3  11420  pfxccat3  11422  swrdccat  11423  pfxccatpfx2  11425  pfxccat3a  11426  swrdccat3blem  11427  swrdccat3b  11428  s2dmg  11478  shftfvalg  11499  shftf  11511  crre  11538  crim  11539  mulreap  11545  readd  11550  resub  11551  remul2  11554  imadd  11558  imsub  11559  immul2  11561  ipcnval  11567  cjsub  11573  cjreim  11584  caucvgre  11662  rexanuz  11669  rexuz3  11671  resqrexlemover  11691  resqrexlemcvg  11700  resqrexlemglsq  11703  sqrtle  11717  sqrtlt  11718  sqrt11ap  11719  sqrt11  11720  absreimsq  11748  absreim  11749  absmul  11750  sqabs  11763  absdiflt  11773  absdifle  11774  abssuble0  11784  abs2difabs  11789  fzomaxdif  11794  caubnd2  11798  rpmaxcl  11904  zmaxcl  11905  nn0maxcl  11906  minmax  11911  mincl  11912  min1inf  11913  min2inf  11914  minabs  11917  minclpr  11918  rpmincl  11919  2zinfmin  11924  xrmaxrecl  11936  xrminmax  11946  xrmincl  11947  xrmin1inf  11948  xrmin2inf  11949  xrminrecl  11954  xrminrpcl  11955  iooinsup  11958  climconst2  11972  climuni  11974  2clim  11982  climshft  11985  climshft2  11987  cjcn2  11997  climaddc1  12010  climmulc2  12012  climsubc1  12013  climsubc2  12014  climlec2  12022  summodclem2a  12063  zsumdc  12066  isumclim3  12105  mptfzshft  12124  fsumrev  12125  fisum0diag2  12129  telfsumo2  12149  fsumparts  12152  cvgcmpub  12158  binomlem  12165  binom1p  12167  binom1dif  12169  bcxmas  12171  isumshft  12172  expcnvap0  12184  expcnv  12186  geosergap  12188  geolim  12193  cvgratnnlemrate  12212  mertenslemi1  12217  mertenslem2  12218  mertensabs  12219  prodmodc  12260  zproddc  12261  fprodf1o  12270  fprodeq0  12299  efcj  12355  eftlub  12372  effsumlt  12374  efieq  12417  sinsub  12422  cossub  12423  subsin  12425  sinmul  12426  cosmul  12427  addcos  12428  subcos  12429  dvdssub2  12517  dvdsadd  12518  dvdsaddr  12519  dvdssub  12520  dvdssubr  12521  fzocongeq  12540  odd2np1  12555  opoe  12577  omoe  12578  opeo  12579  omeo  12580  divalgb  12607  ndvdsadd  12613  bitsfi  12639  gcdmndc  12647  gcdabs  12680  dvdsgcd  12704  absmulgcd  12709  gcdmultiple  12712  gcdmultiplez  12713  rpmulgcd  12718  sqgcd  12721  dvdssqlem  12722  dvdssq  12723  nninfctlemfo  12732  nn0seqcvgd  12734  ialgrlemconst  12736  algrf  12738  algrp1  12739  algcvg  12741  algcvga  12744  lcmval  12756  lcmabs  12769  lcmgcd  12771  lcmdvds  12772  lcmgcdnn  12775  coprmgcdb  12781  coprmdvds  12785  coprmdvds2  12786  qredeq  12789  isprm3  12811  nprm  12816  divgcdodd  12836  prmdvdsexp  12841  sqrt2irr  12855  zgcdsq  12894  hashdvds  12914  phiprmpw  12915  crth  12917  phimullem  12918  modprm0  12948  coprimeprodsq  12951  coprimeprodsq2  12952  pythagtriplem2  12960  pythagtriplem19  12976  pcdvdsb  13014  pcneg  13019  pc2dvds  13024  pc11  13025  pcmpt  13037  pcfac  13044  infpnlem1  13053  prmunb  13056  1arithlem4  13060  1arith  13061  gzaddcl  13071  gzmulcl  13072  gzreim  13073  gzsubcl  13074  4sqlem1  13082  4sqlem4a  13085  4sqlem4  13086  4sqlem12  13096  setsvalg  13234  setsfun0  13240  restval  13450  xpsval  13557  mndinvmod  13650  resmhm  13692  resmhm2  13693  mhmco  13695  dfgrp3m  13804  mhmmnd  13825  mulgnngsum  13836  mulgnn0z  13858  mulgnndir  13860  ghmex  13964  0ghm  13967  resghm  13969  resghm2  13970  ghmco  13973  ghmeql  13976  kerf1ghm  13983  ablsubsub23  14034  dfrhm2  14291  isrhm  14295  rhmfn  14309  rhmval  14310  rhmco  14311  resrhm  14385  rhmeql  14387  rhmima  14388  lmodfopne  14466  lspf  14529  znidom  14797  znrrg  14800  innei  15020  cnovex  15053  txuni2  15113  txbasex  15114  txbas  15115  txtop  15117  txtopon  15119  txss12  15123  txbasval  15124  txcnp  15128  upxp  15129  txcnmpt  15130  uptx  15131  txcn  15132  txrest  15133  txdis  15134  cnmpt21  15148  hmeoco  15173  txhmeo  15176  isxmet2d  15205  blin2  15289  comet  15356  metcn  15371  txmetcn  15376  qtopbasss  15378  qtopbas  15379  remetdval  15404  bl2ioo  15407  blssioo  15410  divcnap  15422  cncfmet  15449  dvaddxxbr  15558  dvcjbr  15565  plyf  15594  ply1termlem  15599  plymullem1  15605  plyaddlem  15606  plymullem  15607  plycolemc  15615  plyreres  15621  dvply1  15622  efle  15633  reapef  15635  sinperlem  15665  sincosq2sgn  15684  sincosq3sgn  15685  sincos6thpi  15699  ioocosf1o  15711  relogoprlem  15725  logleb  15732  cxple3  15778  cxpcom  15795  dvdsppwf1o  15849  fsumdvdsmul  15851  1sgmprm  15854  mersenne  15857  lgslem3  15867  lgsdir2  15898  lgsdir  15900  lgsdilem2  15901  lgsdi  15902  gausslemma2dlem1a  15923  gausslemma2dlem3  15928  gausslemma2dlem6  15932  lgseisenlem3  15937  lgseisenlem4  15938  lgsquadlem1  15942  lgsquadlem2  15943  lgsquad2  15948  lgsquad3  15949  2lgslem1a1  15951  2lgslem1a  15953  2lgslem1c  15955  2sqlem2  15980  mul2sq  15981  2sqlem7  15986  usgredg2v  16211  ushgredgedg  16213  ushgredgedgloop  16215  uhgrissubgr  16248  vtxedgfi  16276  vtxlpfi  16277  wlkeq  16341  uspgr2wlkeq  16352  clwwlkccatlem  16387  clwwlkccat  16388  clwwlknccat  16410  bj-inex  16669  bj-bdfindis  16709  triap  16805  cvgcmp2nlemabs  16808  trilpolemisumle  16814  inffz  16849