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  2247  sylan9eq  2284  csbcomg  3151  sylan9ss  3241  ssconb  3342  ineqan12d  3412  dfopg  3865  breqan12d  4109  opexg  4326  copsex2g  4344  ordin  4488  onin  4489  unexg  4546  eusv1  4555  opelvvg  4781  opthprc  4783  opbrop  4811  relop  4886  dmpropg  5216  unixpm  5279  funssres  5376  funinsn  5386  funtp  5390  fnco  5447  resasplitss  5524  fodmrnu  5576  relrnfvex  5666  funopdmsn  5842  fconst2g  5877  oveqan12d  6047  ovi3  6169  ovg  6171  f1opw2  6239  off  6257  offres  6306  suppfnss  6435  iunon  6493  nnsucsssuc  6703  nnaword1  6724  ertr  6760  erex  6769  brecop  6837  ecovdi  6858  ecovidi  6859  mapvalg  6870  pmvalg  6871  pmss12g  6887  mapsn  6902  en2sn  7031  xpf1o  7073  xpen  7074  phplem4  7084  ssfilem  7105  ssfilemd  7107  diffitest  7119  en1eqsn  7190  sbthlem7  7205  ordiso  7278  updjud  7324  fodju0  7389  finnum  7430  pr2nelem  7439  djucomen  7474  exmidontriimlem1  7479  2onetap  7517  ltsopi  7583  pitric  7584  pitri3or  7585  ltdcpi  7586  mulclpi  7591  addcompig  7592  mulcompig  7594  distrpig  7596  ltexpi  7600  ltapig  7601  ltmpig  7602  dfplpq2  7617  dfmpq2  7618  enqbreq2  7620  enqdc  7624  addcmpblnq  7630  addpipqqslem  7632  mulpipq2  7634  mulpipq  7635  mulpipqqs  7636  addclnq  7638  distrnqg  7650  ltdcnq  7660  ltrnqg  7683  enq0breq  7699  addclnq0  7714  nqnq0a  7717  nqnq0m  7718  nq0m0r  7719  distrnq0  7722  mulcomnq0  7723  genipv  7772  genplt2i  7773  genpelvl  7775  genpelvu  7776  addnqprlemrl  7820  addnqprlemru  7821  addnqprlemfl  7822  addnqprlemfu  7823  addnqpr  7824  mulnqprlemrl  7836  mulnqprlemru  7837  mulnqprlemfl  7838  mulnqprlemfu  7839  mulnqpr  7840  distrlem4prl  7847  distrlem4pru  7848  ltnqpr  7856  recexprlemloc  7894  archrecnq  7926  mulclsr  8017  1idsr  8031  00sr  8032  prsradd  8049  axmulass  8136  axdistr  8137  axcnre  8144  peano5nnnn  8155  mulrid  8219  axltadd  8292  lenlt  8298  cnegexlem3  8399  cnegex  8400  resubcl  8486  subeqrev  8598  muladd  8606  mulsub  8623  mulsub2  8624  ltaddsub2  8660  leaddsub2  8662  leltadd  8670  ltaddpos2  8676  posdif  8678  addge02  8696  mullt0  8703  recexre  8801  recextlem1  8874  recexap  8876  divmuldivap  8935  conjmulap  8952  div2subap  9060  prodgt02  9076  prodge02  9078  lemul2  9080  lemul2a  9082  ltmulgt12  9088  lemulge12  9090  ltmuldiv2  9098  ltdivmul2  9101  ledivmul2  9103  lemuldiv2  9105  negiso  9178  cju  9184  peano5nni  9189  nnaddcl  9206  nnmulcl  9207  nnsub  9225  addltmul  9424  avgle1  9428  avgle2  9429  nnrecl  9443  nn0nnaddcl  9476  zsubcl  9563  zleloe  9569  znnsub  9574  nzadd  9575  zmulcl  9576  zltp1le  9577  zleltp1  9578  nnleltp1  9582  nnltp1le  9583  nnaddm1cl  9584  nn0ltp1le  9585  nn0leltp1  9586  nn0ltlem1  9587  znn0sub  9588  nn0sub  9589  elz2  9594  zapne  9597  zdcle  9599  zdclt  9600  zltlen  9601  nn0lem1lt  9606  nnlem1lt  9607  nnltlem1  9608  zdiv  9611  zextle  9614  zextlt  9615  btwnnz  9617  prime  9622  nneo  9626  peano2uz2  9630  peano5uzti  9631  uzind  9634  fzind  9638  fnn0ind  9639  uzneg  9818  uz11  9822  eluzp1m1  9823  eluzp1p1  9825  uzin  9832  indstr  9870  uz2mulcl  9885  qre  9902  qaddcl  9912  qsubcl  9915  qltlen  9917  qlttri2  9918  irradd  9923  elpqb  9927  cnref1o  9928  rpaddcl  9955  rpmulcl  9956  rpdivcl  9957  rexadd  10130  rexsub  10131  xaddcom  10139  xnn0xadd0  10145  xnegdi  10146  elicc2  10216  iccshftr  10272  iccshftl  10274  iccdil  10276  icccntr  10278  fzval2  10289  elfz1eq  10313  peano2fzr  10315  fznlem  10319  fzsplit2  10328  fzaddel  10337  fzsubel  10338  fzrev2  10363  fzrev3  10365  uzsplit  10370  fzrevral  10383  fzrevral3  10385  fzshftral  10386  elfz2nn0  10390  fznn0sub2  10406  fz0fzdiffz0  10408  elfzmlbp  10410  difelfzle  10412  difelfznle  10413  1fv  10417  elfzouz2  10440  fzo0n  10446  fzouzsplit  10459  fzoun  10461  elfzo0le  10468  fzonmapblen  10470  fzofzim  10471  fzoaddel2  10479  eluzgtdifelfzo  10486  elfzodifsumelfzo  10490  ubmelm1fzo  10515  fzofzp1b  10517  fzosplitprm1  10524  fzostep1  10527  subfzo0  10532  zsupcllemstep  10533  qdclt  10549  qbtwnxr  10561  flqbi2  10595  divfl0  10600  flqzadd  10602  flqmulnn0  10603  addmodidr  10679  modfzo0difsn  10701  frec2uzltd  10709  frec2uzrand  10711  frecfzen2  10733  seqshft2g  10788  seq3split  10794  seqsplitg  10795  seq3caopr2  10799  seqcaopr2g  10800  seqf1oglem2  10826  exp3vallem  10846  expcllem  10856  expcl2lemap  10857  1exp  10874  expge1  10882  expadd  10887  expmul  10890  expsubap  10893  leexp1a  10900  lt2sq  10919  le2sq  10920  sumsqeq0  10924  qsqeqor  10956  bernneq  10966  bernneq2  10967  sq11ap  11013  facdiv  11044  faclbnd  11047  faclbnd3  11049  faclbnd6  11050  facavg  11052  bcrpcl  11059  bccmpl  11060  fiubm  11136  seq3coll  11150  eqwrd  11201  ccatcl  11217  ccatclab  11218  ccatlen  11219  ccat0  11220  ccatval1  11221  ccatval2  11222  elfzelfzccat  11224  ccatvalfn  11225  ccatsymb  11226  ccatval21sw  11229  ccatrn  11233  lswccatn0lsw  11235  ccatalpha  11237  ccatrcl1  11238  swrdfv2  11291  swrdsbslen  11294  swrdspsleq  11295  swrdccat2  11299  pfxclz  11307  ccatpfx  11329  pfxccat1  11330  swrdswrdlem  11332  pfxswrd  11334  pfxccatin12lem4  11354  pfxccatin12lem1  11356  pfxccatin12lem2  11359  pfxccatin12lem3  11360  pfxccat3  11362  swrdccat  11363  pfxccatpfx2  11365  pfxccat3a  11366  swrdccat3blem  11367  swrdccat3b  11368  s2dmg  11418  shftfvalg  11439  shftf  11451  crre  11478  crim  11479  mulreap  11485  readd  11490  resub  11491  remul2  11494  imadd  11498  imsub  11499  immul2  11501  ipcnval  11507  cjsub  11513  cjreim  11524  caucvgre  11602  rexanuz  11609  rexuz3  11611  resqrexlemover  11631  resqrexlemcvg  11640  resqrexlemglsq  11643  sqrtle  11657  sqrtlt  11658  sqrt11ap  11659  sqrt11  11660  absreimsq  11688  absreim  11689  absmul  11690  sqabs  11703  absdiflt  11713  absdifle  11714  abssuble0  11724  abs2difabs  11729  fzomaxdif  11734  caubnd2  11738  rpmaxcl  11844  zmaxcl  11845  nn0maxcl  11846  minmax  11851  mincl  11852  min1inf  11853  min2inf  11854  minabs  11857  minclpr  11858  rpmincl  11859  2zinfmin  11864  xrmaxrecl  11876  xrminmax  11886  xrmincl  11887  xrmin1inf  11888  xrmin2inf  11889  xrminrecl  11894  xrminrpcl  11895  iooinsup  11898  climconst2  11912  climuni  11914  2clim  11922  climshft  11925  climshft2  11927  cjcn2  11937  climaddc1  11950  climmulc2  11952  climsubc1  11953  climsubc2  11954  climlec2  11962  summodclem2a  12003  zsumdc  12006  isumclim3  12045  mptfzshft  12064  fsumrev  12065  fisum0diag2  12069  telfsumo2  12089  fsumparts  12092  cvgcmpub  12098  binomlem  12105  binom1p  12107  binom1dif  12109  bcxmas  12111  isumshft  12112  expcnvap0  12124  expcnv  12126  geosergap  12128  geolim  12133  cvgratnnlemrate  12152  mertenslemi1  12157  mertenslem2  12158  mertensabs  12159  prodmodc  12200  zproddc  12201  fprodf1o  12210  fprodeq0  12239  efcj  12295  eftlub  12312  effsumlt  12314  efieq  12357  sinsub  12362  cossub  12363  subsin  12365  sinmul  12366  cosmul  12367  addcos  12368  subcos  12369  dvdssub2  12457  dvdsadd  12458  dvdsaddr  12459  dvdssub  12460  dvdssubr  12461  fzocongeq  12480  odd2np1  12495  opoe  12517  omoe  12518  opeo  12519  omeo  12520  divalgb  12547  ndvdsadd  12553  bitsfi  12579  gcdmndc  12587  gcdabs  12620  dvdsgcd  12644  absmulgcd  12649  gcdmultiple  12652  gcdmultiplez  12653  rpmulgcd  12658  sqgcd  12661  dvdssqlem  12662  dvdssq  12663  nninfctlemfo  12672  nn0seqcvgd  12674  ialgrlemconst  12676  algrf  12678  algrp1  12679  algcvg  12681  algcvga  12684  lcmval  12696  lcmabs  12709  lcmgcd  12711  lcmdvds  12712  lcmgcdnn  12715  coprmgcdb  12721  coprmdvds  12725  coprmdvds2  12726  qredeq  12729  isprm3  12751  nprm  12756  divgcdodd  12776  prmdvdsexp  12781  sqrt2irr  12795  zgcdsq  12834  hashdvds  12854  phiprmpw  12855  crth  12857  phimullem  12858  modprm0  12888  coprimeprodsq  12891  coprimeprodsq2  12892  pythagtriplem2  12900  pythagtriplem19  12916  pcdvdsb  12954  pcneg  12959  pc2dvds  12964  pc11  12965  pcmpt  12977  pcfac  12984  infpnlem1  12993  prmunb  12996  1arithlem4  13000  1arith  13001  gzaddcl  13011  gzmulcl  13012  gzreim  13013  gzsubcl  13014  4sqlem1  13022  4sqlem4a  13025  4sqlem4  13026  4sqlem12  13036  setsvalg  13173  setsfun0  13179  restval  13389  xpsval  13496  mndinvmod  13589  resmhm  13631  resmhm2  13632  mhmco  13634  dfgrp3m  13743  mhmmnd  13764  mulgnngsum  13775  mulgnn0z  13797  mulgnndir  13799  ghmex  13903  0ghm  13906  resghm  13908  resghm2  13909  ghmco  13912  ghmeql  13915  kerf1ghm  13922  ablsubsub23  13973  dfrhm2  14230  isrhm  14234  rhmfn  14248  rhmval  14249  rhmco  14250  resrhm  14324  rhmeql  14326  rhmima  14327  lmodfopne  14402  lspf  14465  znidom  14733  znrrg  14736  innei  14954  cnovex  14987  txuni2  15047  txbasex  15048  txbas  15049  txtop  15051  txtopon  15053  txss12  15057  txbasval  15058  txcnp  15062  upxp  15063  txcnmpt  15064  uptx  15065  txcn  15066  txrest  15067  txdis  15068  cnmpt21  15082  hmeoco  15107  txhmeo  15110  isxmet2d  15139  blin2  15223  comet  15290  metcn  15305  txmetcn  15310  qtopbasss  15312  qtopbas  15313  remetdval  15338  bl2ioo  15341  blssioo  15344  divcnap  15356  cncfmet  15383  dvaddxxbr  15492  dvcjbr  15499  plyf  15528  ply1termlem  15533  plymullem1  15539  plyaddlem  15540  plymullem  15541  plycolemc  15549  plyreres  15555  dvply1  15556  efle  15567  reapef  15569  sinperlem  15599  sincosq2sgn  15618  sincosq3sgn  15619  sincos6thpi  15633  ioocosf1o  15645  relogoprlem  15659  logleb  15666  cxple3  15712  cxpcom  15729  dvdsppwf1o  15783  fsumdvdsmul  15785  1sgmprm  15788  mersenne  15791  lgslem3  15801  lgsdir2  15832  lgsdir  15834  lgsdilem2  15835  lgsdi  15836  gausslemma2dlem1a  15857  gausslemma2dlem3  15862  gausslemma2dlem6  15866  lgseisenlem3  15871  lgseisenlem4  15872  lgsquadlem1  15876  lgsquadlem2  15877  lgsquad2  15882  lgsquad3  15883  2lgslem1a1  15885  2lgslem1a  15887  2lgslem1c  15889  2sqlem2  15914  mul2sq  15915  2sqlem7  15920  usgredg2v  16145  ushgredgedg  16147  ushgredgedgloop  16149  uhgrissubgr  16182  vtxedgfi  16210  vtxlpfi  16211  wlkeq  16275  uspgr2wlkeq  16286  clwwlkccatlem  16321  clwwlkccat  16322  clwwlknccat  16344  bj-inex  16603  bj-bdfindis  16643  triap  16741  cvgcmp2nlemabs  16744  trilpolemisumle  16750  inffz  16785