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  947  mp3an3an  1379  eqeqan12d  2247  sylan9eq  2284  csbcomg  3150  sylan9ss  3240  ssconb  3340  ineqan12d  3410  dfopg  3860  breqan12d  4104  opexg  4320  copsex2g  4338  ordin  4482  onin  4483  unexg  4540  eusv1  4549  opelvvg  4775  opthprc  4777  opbrop  4805  relop  4880  dmpropg  5209  unixpm  5272  funssres  5369  funinsn  5379  funtp  5383  fnco  5440  resasplitss  5516  fodmrnu  5567  relrnfvex  5657  funopdmsn  5834  fconst2g  5869  oveqan12d  6037  ovi3  6159  ovg  6161  f1opw2  6229  off  6248  offres  6297  iunon  6450  nnsucsssuc  6660  nnaword1  6681  ertr  6717  erex  6726  brecop  6794  ecovdi  6815  ecovidi  6816  mapvalg  6827  pmvalg  6828  pmss12g  6844  mapsn  6859  en2sn  6988  xpf1o  7030  xpen  7031  phplem4  7041  ssfilem  7062  ssfilemd  7064  diffitest  7076  en1eqsn  7147  sbthlem7  7162  ordiso  7235  updjud  7281  fodju0  7346  finnum  7387  pr2nelem  7396  djucomen  7431  exmidontriimlem1  7436  2onetap  7474  ltsopi  7540  pitric  7541  pitri3or  7542  ltdcpi  7543  mulclpi  7548  addcompig  7549  mulcompig  7551  distrpig  7553  ltexpi  7557  ltapig  7558  ltmpig  7559  dfplpq2  7574  dfmpq2  7575  enqbreq2  7577  enqdc  7581  addcmpblnq  7587  addpipqqslem  7589  mulpipq2  7591  mulpipq  7592  mulpipqqs  7593  addclnq  7595  distrnqg  7607  ltdcnq  7617  ltrnqg  7640  enq0breq  7656  addclnq0  7671  nqnq0a  7674  nqnq0m  7675  nq0m0r  7676  distrnq0  7679  mulcomnq0  7680  genipv  7729  genplt2i  7730  genpelvl  7732  genpelvu  7733  addnqprlemrl  7777  addnqprlemru  7778  addnqprlemfl  7779  addnqprlemfu  7780  addnqpr  7781  mulnqprlemrl  7793  mulnqprlemru  7794  mulnqprlemfl  7795  mulnqprlemfu  7796  mulnqpr  7797  distrlem4prl  7804  distrlem4pru  7805  ltnqpr  7813  recexprlemloc  7851  archrecnq  7883  mulclsr  7974  1idsr  7988  00sr  7989  prsradd  8006  axmulass  8093  axdistr  8094  axcnre  8101  peano5nnnn  8112  mulrid  8176  axltadd  8249  lenlt  8255  cnegexlem3  8356  cnegex  8357  resubcl  8443  subeqrev  8555  muladd  8563  mulsub  8580  mulsub2  8581  ltaddsub2  8617  leaddsub2  8619  leltadd  8627  ltaddpos2  8633  posdif  8635  addge02  8653  mullt0  8660  recexre  8758  recextlem1  8831  recexap  8833  divmuldivap  8892  conjmulap  8909  div2subap  9017  prodgt02  9033  prodge02  9035  lemul2  9037  lemul2a  9039  ltmulgt12  9045  lemulge12  9047  ltmuldiv2  9055  ltdivmul2  9058  ledivmul2  9060  lemuldiv2  9062  negiso  9135  cju  9141  peano5nni  9146  nnaddcl  9163  nnmulcl  9164  nnsub  9182  addltmul  9381  avgle1  9385  avgle2  9386  nnrecl  9400  nn0nnaddcl  9433  zsubcl  9520  zleloe  9526  znnsub  9531  nzadd  9532  zmulcl  9533  zltp1le  9534  zleltp1  9535  nnleltp1  9539  nnltp1le  9540  nnaddm1cl  9541  nn0ltp1le  9542  nn0leltp1  9543  nn0ltlem1  9544  znn0sub  9545  nn0sub  9546  elz2  9551  zapne  9554  zdcle  9556  zdclt  9557  zltlen  9558  nn0lem1lt  9563  nnlem1lt  9564  nnltlem1  9565  zdiv  9568  zextle  9571  zextlt  9572  btwnnz  9574  prime  9579  nneo  9583  peano2uz2  9587  peano5uzti  9588  uzind  9591  fzind  9595  fnn0ind  9596  uzneg  9775  uz11  9779  eluzp1m1  9780  eluzp1p1  9782  uzin  9789  indstr  9827  uz2mulcl  9842  qre  9859  qaddcl  9869  qsubcl  9872  qltlen  9874  qlttri2  9875  irradd  9880  elpqb  9884  cnref1o  9885  rpaddcl  9912  rpmulcl  9913  rpdivcl  9914  rexadd  10087  rexsub  10088  xaddcom  10096  xnn0xadd0  10102  xnegdi  10103  elicc2  10173  iccshftr  10229  iccshftl  10231  iccdil  10233  icccntr  10235  fzval2  10246  elfz1eq  10270  peano2fzr  10272  fznlem  10276  fzsplit2  10285  fzaddel  10294  fzsubel  10295  fzrev2  10320  fzrev3  10322  uzsplit  10327  fzrevral  10340  fzrevral3  10342  fzshftral  10343  elfz2nn0  10347  fznn0sub2  10363  fz0fzdiffz0  10365  elfzmlbp  10367  difelfzle  10369  difelfznle  10370  1fv  10374  elfzouz2  10397  fzo0n  10403  fzouzsplit  10416  fzoun  10418  elfzo0le  10425  fzonmapblen  10427  fzofzim  10428  fzoaddel2  10436  eluzgtdifelfzo  10443  elfzodifsumelfzo  10447  ubmelm1fzo  10472  fzofzp1b  10474  fzosplitprm1  10481  fzostep1  10484  subfzo0  10489  zsupcllemstep  10490  qdclt  10506  qbtwnxr  10518  flqbi2  10552  divfl0  10557  flqzadd  10559  flqmulnn0  10560  addmodidr  10636  modfzo0difsn  10658  frec2uzltd  10666  frec2uzrand  10668  frecfzen2  10690  seqshft2g  10745  seq3split  10751  seqsplitg  10752  seq3caopr2  10756  seqcaopr2g  10757  seqf1oglem2  10783  exp3vallem  10803  expcllem  10813  expcl2lemap  10814  1exp  10831  expge1  10839  expadd  10844  expmul  10847  expsubap  10850  leexp1a  10857  lt2sq  10876  le2sq  10877  sumsqeq0  10881  qsqeqor  10913  bernneq  10923  bernneq2  10924  sq11ap  10970  facdiv  11001  faclbnd  11004  faclbnd3  11006  faclbnd6  11007  facavg  11009  bcrpcl  11016  bccmpl  11017  fiubm  11093  seq3coll  11107  eqwrd  11158  ccatcl  11174  ccatclab  11175  ccatlen  11176  ccat0  11177  ccatval1  11178  ccatval2  11179  elfzelfzccat  11181  ccatvalfn  11182  ccatsymb  11183  ccatval21sw  11186  ccatrn  11190  lswccatn0lsw  11192  ccatalpha  11194  ccatrcl1  11195  swrdfv2  11248  swrdsbslen  11251  swrdspsleq  11252  swrdccat2  11256  pfxclz  11264  ccatpfx  11286  pfxccat1  11287  swrdswrdlem  11289  pfxswrd  11291  pfxccatin12lem4  11311  pfxccatin12lem1  11313  pfxccatin12lem2  11316  pfxccatin12lem3  11317  pfxccat3  11319  swrdccat  11320  pfxccatpfx2  11322  pfxccat3a  11323  swrdccat3blem  11324  swrdccat3b  11325  s2dmg  11375  shftfvalg  11383  shftf  11395  crre  11422  crim  11423  mulreap  11429  readd  11434  resub  11435  remul2  11438  imadd  11442  imsub  11443  immul2  11445  ipcnval  11451  cjsub  11457  cjreim  11468  caucvgre  11546  rexanuz  11553  rexuz3  11555  resqrexlemover  11575  resqrexlemcvg  11584  resqrexlemglsq  11587  sqrtle  11601  sqrtlt  11602  sqrt11ap  11603  sqrt11  11604  absreimsq  11632  absreim  11633  absmul  11634  sqabs  11647  absdiflt  11657  absdifle  11658  abssuble0  11668  abs2difabs  11673  fzomaxdif  11678  caubnd2  11682  rpmaxcl  11788  zmaxcl  11789  nn0maxcl  11790  minmax  11795  mincl  11796  min1inf  11797  min2inf  11798  minabs  11801  minclpr  11802  rpmincl  11803  2zinfmin  11808  xrmaxrecl  11820  xrminmax  11830  xrmincl  11831  xrmin1inf  11832  xrmin2inf  11833  xrminrecl  11838  xrminrpcl  11839  iooinsup  11842  climconst2  11856  climuni  11858  2clim  11866  climshft  11869  climshft2  11871  cjcn2  11881  climaddc1  11894  climmulc2  11896  climsubc1  11897  climsubc2  11898  climlec2  11906  summodclem2a  11947  zsumdc  11950  isumclim3  11989  mptfzshft  12008  fsumrev  12009  fisum0diag2  12013  telfsumo2  12033  fsumparts  12036  cvgcmpub  12042  binomlem  12049  binom1p  12051  binom1dif  12053  bcxmas  12055  isumshft  12056  expcnvap0  12068  expcnv  12070  geosergap  12072  geolim  12077  cvgratnnlemrate  12096  mertenslemi1  12101  mertenslem2  12102  mertensabs  12103  prodmodc  12144  zproddc  12145  fprodf1o  12154  fprodeq0  12183  efcj  12239  eftlub  12256  effsumlt  12258  efieq  12301  sinsub  12306  cossub  12307  subsin  12309  sinmul  12310  cosmul  12311  addcos  12312  subcos  12313  dvdssub2  12401  dvdsadd  12402  dvdsaddr  12403  dvdssub  12404  dvdssubr  12405  fzocongeq  12424  odd2np1  12439  opoe  12461  omoe  12462  opeo  12463  omeo  12464  divalgb  12491  ndvdsadd  12497  bitsfi  12523  gcdmndc  12531  gcdabs  12564  dvdsgcd  12588  absmulgcd  12593  gcdmultiple  12596  gcdmultiplez  12597  rpmulgcd  12602  sqgcd  12605  dvdssqlem  12606  dvdssq  12607  nninfctlemfo  12616  nn0seqcvgd  12618  ialgrlemconst  12620  algrf  12622  algrp1  12623  algcvg  12625  algcvga  12628  lcmval  12640  lcmabs  12653  lcmgcd  12655  lcmdvds  12656  lcmgcdnn  12659  coprmgcdb  12665  coprmdvds  12669  coprmdvds2  12670  qredeq  12673  isprm3  12695  nprm  12700  divgcdodd  12720  prmdvdsexp  12725  sqrt2irr  12739  zgcdsq  12778  hashdvds  12798  phiprmpw  12799  crth  12801  phimullem  12802  modprm0  12832  coprimeprodsq  12835  coprimeprodsq2  12836  pythagtriplem2  12844  pythagtriplem19  12860  pcdvdsb  12898  pcneg  12903  pc2dvds  12908  pc11  12909  pcmpt  12921  pcfac  12928  infpnlem1  12937  prmunb  12940  1arithlem4  12944  1arith  12945  gzaddcl  12955  gzmulcl  12956  gzreim  12957  gzsubcl  12958  4sqlem1  12966  4sqlem4a  12969  4sqlem4  12970  4sqlem12  12980  setsvalg  13117  setsfun0  13123  restval  13333  xpsval  13440  mndinvmod  13533  resmhm  13575  resmhm2  13576  mhmco  13578  dfgrp3m  13687  mhmmnd  13708  mulgnngsum  13719  mulgnn0z  13741  mulgnndir  13743  ghmex  13847  0ghm  13850  resghm  13852  resghm2  13853  ghmco  13856  ghmeql  13859  kerf1ghm  13866  ablsubsub23  13917  dfrhm2  14174  isrhm  14178  rhmfn  14192  rhmval  14193  rhmco  14194  resrhm  14268  rhmeql  14270  rhmima  14271  lmodfopne  14346  lspf  14409  znidom  14677  znrrg  14680  innei  14893  cnovex  14926  txuni2  14986  txbasex  14987  txbas  14988  txtop  14990  txtopon  14992  txss12  14996  txbasval  14997  txcnp  15001  upxp  15002  txcnmpt  15003  uptx  15004  txcn  15005  txrest  15006  txdis  15007  cnmpt21  15021  hmeoco  15046  txhmeo  15049  isxmet2d  15078  blin2  15162  comet  15229  metcn  15244  txmetcn  15249  qtopbasss  15251  qtopbas  15252  remetdval  15277  bl2ioo  15280  blssioo  15283  divcnap  15295  cncfmet  15322  dvaddxxbr  15431  dvcjbr  15438  plyf  15467  ply1termlem  15472  plymullem1  15478  plyaddlem  15479  plymullem  15480  plycolemc  15488  plyreres  15494  dvply1  15495  efle  15506  reapef  15508  sinperlem  15538  sincosq2sgn  15557  sincosq3sgn  15558  sincos6thpi  15572  ioocosf1o  15584  relogoprlem  15598  logleb  15605  cxple3  15651  cxpcom  15668  dvdsppwf1o  15719  fsumdvdsmul  15721  1sgmprm  15724  mersenne  15727  lgslem3  15737  lgsdir2  15768  lgsdir  15770  lgsdilem2  15771  lgsdi  15772  gausslemma2dlem1a  15793  gausslemma2dlem3  15798  gausslemma2dlem6  15802  lgseisenlem3  15807  lgseisenlem4  15808  lgsquadlem1  15812  lgsquadlem2  15813  lgsquad2  15818  lgsquad3  15819  2lgslem1a1  15821  2lgslem1a  15823  2lgslem1c  15825  2sqlem2  15850  mul2sq  15851  2sqlem7  15856  usgredg2v  16081  ushgredgedg  16083  ushgredgedgloop  16085  uhgrissubgr  16118  vtxedgfi  16146  vtxlpfi  16147  wlkeq  16211  uspgr2wlkeq  16222  clwwlkccatlem  16257  clwwlkccat  16258  clwwlknccat  16280  bj-inex  16528  bj-bdfindis  16568  triap  16659  cvgcmp2nlemabs  16662  trilpolemisumle  16668  inffz  16702