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  596  syl2an2r  597  orandc  945  mp3an3an  1377  eqeqan12d  2245  sylan9eq  2282  csbcomg  3148  sylan9ss  3238  ssconb  3338  ineqan12d  3408  dfopg  3856  breqan12d  4100  opexg  4316  copsex2g  4334  ordin  4478  onin  4479  unexg  4536  eusv1  4545  opelvvg  4771  opthprc  4773  opbrop  4801  relop  4876  dmpropg  5205  unixpm  5268  funssres  5364  funinsn  5374  funtp  5378  fnco  5435  resasplitss  5511  fodmrnu  5562  relrnfvex  5651  funopdmsn  5827  fconst2g  5862  oveqan12d  6030  ovi3  6152  ovg  6154  f1opw2  6222  off  6241  offres  6290  iunon  6443  nnsucsssuc  6653  nnaword1  6674  ertr  6710  erex  6719  brecop  6787  ecovdi  6808  ecovidi  6809  mapvalg  6820  pmvalg  6821  pmss12g  6837  mapsn  6852  en2sn  6981  xpf1o  7023  xpen  7024  phplem4  7034  ssfilem  7055  diffitest  7067  en1eqsn  7136  sbthlem7  7151  ordiso  7224  updjud  7270  fodju0  7335  finnum  7376  pr2nelem  7385  djucomen  7419  exmidontriimlem1  7424  2onetap  7462  ltsopi  7528  pitric  7529  pitri3or  7530  ltdcpi  7531  mulclpi  7536  addcompig  7537  mulcompig  7539  distrpig  7541  ltexpi  7545  ltapig  7546  ltmpig  7547  dfplpq2  7562  dfmpq2  7563  enqbreq2  7565  enqdc  7569  addcmpblnq  7575  addpipqqslem  7577  mulpipq2  7579  mulpipq  7580  mulpipqqs  7581  addclnq  7583  distrnqg  7595  ltdcnq  7605  ltrnqg  7628  enq0breq  7644  addclnq0  7659  nqnq0a  7662  nqnq0m  7663  nq0m0r  7664  distrnq0  7667  mulcomnq0  7668  genipv  7717  genplt2i  7718  genpelvl  7720  genpelvu  7721  addnqprlemrl  7765  addnqprlemru  7766  addnqprlemfl  7767  addnqprlemfu  7768  addnqpr  7769  mulnqprlemrl  7781  mulnqprlemru  7782  mulnqprlemfl  7783  mulnqprlemfu  7784  mulnqpr  7785  distrlem4prl  7792  distrlem4pru  7793  ltnqpr  7801  recexprlemloc  7839  archrecnq  7871  mulclsr  7962  1idsr  7976  00sr  7977  prsradd  7994  axmulass  8081  axdistr  8082  axcnre  8089  peano5nnnn  8100  mulrid  8164  axltadd  8237  lenlt  8243  cnegexlem3  8344  cnegex  8345  resubcl  8431  subeqrev  8543  muladd  8551  mulsub  8568  mulsub2  8569  ltaddsub2  8605  leaddsub2  8607  leltadd  8615  ltaddpos2  8621  posdif  8623  addge02  8641  mullt0  8648  recexre  8746  recextlem1  8819  recexap  8821  divmuldivap  8880  conjmulap  8897  div2subap  9005  prodgt02  9021  prodge02  9023  lemul2  9025  lemul2a  9027  ltmulgt12  9033  lemulge12  9035  ltmuldiv2  9043  ltdivmul2  9046  ledivmul2  9048  lemuldiv2  9050  negiso  9123  cju  9129  peano5nni  9134  nnaddcl  9151  nnmulcl  9152  nnsub  9170  addltmul  9369  avgle1  9373  avgle2  9374  nnrecl  9388  nn0nnaddcl  9421  zsubcl  9508  zleloe  9514  znnsub  9519  nzadd  9520  zmulcl  9521  zltp1le  9522  zleltp1  9523  nnleltp1  9527  nnltp1le  9528  nnaddm1cl  9529  nn0ltp1le  9530  nn0leltp1  9531  nn0ltlem1  9532  znn0sub  9533  nn0sub  9534  elz2  9539  zapne  9542  zdcle  9544  zdclt  9545  zltlen  9546  nn0lem1lt  9551  nnlem1lt  9552  nnltlem1  9553  zdiv  9556  zextle  9559  zextlt  9560  btwnnz  9562  prime  9567  nneo  9571  peano2uz2  9575  peano5uzti  9576  uzind  9579  fzind  9583  fnn0ind  9584  uzneg  9763  uz11  9767  eluzp1m1  9768  eluzp1p1  9770  uzin  9777  indstr  9815  uz2mulcl  9830  qre  9847  qaddcl  9857  qsubcl  9860  qltlen  9862  qlttri2  9863  irradd  9868  elpqb  9872  cnref1o  9873  rpaddcl  9900  rpmulcl  9901  rpdivcl  9902  rexadd  10075  rexsub  10076  xaddcom  10084  xnn0xadd0  10090  xnegdi  10091  elicc2  10161  iccshftr  10217  iccshftl  10219  iccdil  10221  icccntr  10223  fzval2  10234  elfz1eq  10258  peano2fzr  10260  fznlem  10264  fzsplit2  10273  fzaddel  10282  fzsubel  10283  fzrev2  10308  fzrev3  10310  uzsplit  10315  fzrevral  10328  fzrevral3  10330  fzshftral  10331  elfz2nn0  10335  fznn0sub2  10351  fz0fzdiffz0  10353  elfzmlbp  10355  difelfzle  10357  difelfznle  10358  1fv  10362  elfzouz2  10385  fzo0n  10391  fzouzsplit  10404  fzoun  10406  elfzo0le  10412  fzonmapblen  10414  fzofzim  10415  fzoaddel2  10423  eluzgtdifelfzo  10430  elfzodifsumelfzo  10434  ubmelm1fzo  10459  fzofzp1b  10461  fzosplitprm1  10468  fzostep1  10471  subfzo0  10476  zsupcllemstep  10477  qdclt  10493  qbtwnxr  10505  flqbi2  10539  divfl0  10544  flqzadd  10546  flqmulnn0  10547  addmodidr  10623  modfzo0difsn  10645  frec2uzltd  10653  frec2uzrand  10655  frecfzen2  10677  seqshft2g  10732  seq3split  10738  seqsplitg  10739  seq3caopr2  10743  seqcaopr2g  10744  seqf1oglem2  10770  exp3vallem  10790  expcllem  10800  expcl2lemap  10801  1exp  10818  expge1  10826  expadd  10831  expmul  10834  expsubap  10837  leexp1a  10844  lt2sq  10863  le2sq  10864  sumsqeq0  10868  qsqeqor  10900  bernneq  10910  bernneq2  10911  sq11ap  10957  facdiv  10988  faclbnd  10991  faclbnd3  10993  faclbnd6  10994  facavg  10996  bcrpcl  11003  bccmpl  11004  fiubm  11079  seq3coll  11093  eqwrd  11141  ccatcl  11157  ccatclab  11158  ccatlen  11159  ccat0  11160  ccatval1  11161  ccatval2  11162  elfzelfzccat  11164  ccatvalfn  11165  ccatsymb  11166  ccatval21sw  11169  ccatrn  11173  lswccatn0lsw  11175  ccatalpha  11177  ccatrcl1  11178  swrdfv2  11231  swrdsbslen  11234  swrdspsleq  11235  swrdccat2  11239  pfxclz  11247  ccatpfx  11269  pfxccat1  11270  swrdswrdlem  11272  pfxswrd  11274  pfxccatin12lem4  11294  pfxccatin12lem1  11296  pfxccatin12lem2  11299  pfxccatin12lem3  11300  pfxccat3  11302  swrdccat  11303  pfxccatpfx2  11305  pfxccat3a  11306  swrdccat3blem  11307  swrdccat3b  11308  s2dmg  11358  shftfvalg  11366  shftf  11378  crre  11405  crim  11406  mulreap  11412  readd  11417  resub  11418  remul2  11421  imadd  11425  imsub  11426  immul2  11428  ipcnval  11434  cjsub  11440  cjreim  11451  caucvgre  11529  rexanuz  11536  rexuz3  11538  resqrexlemover  11558  resqrexlemcvg  11567  resqrexlemglsq  11570  sqrtle  11584  sqrtlt  11585  sqrt11ap  11586  sqrt11  11587  absreimsq  11615  absreim  11616  absmul  11617  sqabs  11630  absdiflt  11640  absdifle  11641  abssuble0  11651  abs2difabs  11656  fzomaxdif  11661  caubnd2  11665  rpmaxcl  11771  zmaxcl  11772  nn0maxcl  11773  minmax  11778  mincl  11779  min1inf  11780  min2inf  11781  minabs  11784  minclpr  11785  rpmincl  11786  2zinfmin  11791  xrmaxrecl  11803  xrminmax  11813  xrmincl  11814  xrmin1inf  11815  xrmin2inf  11816  xrminrecl  11821  xrminrpcl  11822  iooinsup  11825  climconst2  11839  climuni  11841  2clim  11849  climshft  11852  climshft2  11854  cjcn2  11864  climaddc1  11877  climmulc2  11879  climsubc1  11880  climsubc2  11881  climlec2  11889  summodclem2a  11929  zsumdc  11932  isumclim3  11971  mptfzshft  11990  fsumrev  11991  fisum0diag2  11995  telfsumo2  12015  fsumparts  12018  cvgcmpub  12024  binomlem  12031  binom1p  12033  binom1dif  12035  bcxmas  12037  isumshft  12038  expcnvap0  12050  expcnv  12052  geosergap  12054  geolim  12059  cvgratnnlemrate  12078  mertenslemi1  12083  mertenslem2  12084  mertensabs  12085  prodmodc  12126  zproddc  12127  fprodf1o  12136  fprodeq0  12165  efcj  12221  eftlub  12238  effsumlt  12240  efieq  12283  sinsub  12288  cossub  12289  subsin  12291  sinmul  12292  cosmul  12293  addcos  12294  subcos  12295  dvdssub2  12383  dvdsadd  12384  dvdsaddr  12385  dvdssub  12386  dvdssubr  12387  fzocongeq  12406  odd2np1  12421  opoe  12443  omoe  12444  opeo  12445  omeo  12446  divalgb  12473  ndvdsadd  12479  bitsfi  12505  gcdmndc  12513  gcdabs  12546  dvdsgcd  12570  absmulgcd  12575  gcdmultiple  12578  gcdmultiplez  12579  rpmulgcd  12584  sqgcd  12587  dvdssqlem  12588  dvdssq  12589  nninfctlemfo  12598  nn0seqcvgd  12600  ialgrlemconst  12602  algrf  12604  algrp1  12605  algcvg  12607  algcvga  12610  lcmval  12622  lcmabs  12635  lcmgcd  12637  lcmdvds  12638  lcmgcdnn  12641  coprmgcdb  12647  coprmdvds  12651  coprmdvds2  12652  qredeq  12655  isprm3  12677  nprm  12682  divgcdodd  12702  prmdvdsexp  12707  sqrt2irr  12721  zgcdsq  12760  hashdvds  12780  phiprmpw  12781  crth  12783  phimullem  12784  modprm0  12814  coprimeprodsq  12817  coprimeprodsq2  12818  pythagtriplem2  12826  pythagtriplem19  12842  pcdvdsb  12880  pcneg  12885  pc2dvds  12890  pc11  12891  pcmpt  12903  pcfac  12910  infpnlem1  12919  prmunb  12922  1arithlem4  12926  1arith  12927  gzaddcl  12937  gzmulcl  12938  gzreim  12939  gzsubcl  12940  4sqlem1  12948  4sqlem4a  12951  4sqlem4  12952  4sqlem12  12962  setsvalg  13099  setsfun0  13105  restval  13315  xpsval  13422  mndinvmod  13515  resmhm  13557  resmhm2  13558  mhmco  13560  dfgrp3m  13669  mhmmnd  13690  mulgnngsum  13701  mulgnn0z  13723  mulgnndir  13725  ghmex  13829  0ghm  13832  resghm  13834  resghm2  13835  ghmco  13838  ghmeql  13841  kerf1ghm  13848  ablsubsub23  13899  dfrhm2  14155  isrhm  14159  rhmfn  14173  rhmval  14174  rhmco  14175  resrhm  14249  rhmeql  14251  rhmima  14252  lmodfopne  14327  lspf  14390  znidom  14658  znrrg  14661  innei  14874  cnovex  14907  txuni2  14967  txbasex  14968  txbas  14969  txtop  14971  txtopon  14973  txss12  14977  txbasval  14978  txcnp  14982  upxp  14983  txcnmpt  14984  uptx  14985  txcn  14986  txrest  14987  txdis  14988  cnmpt21  15002  hmeoco  15027  txhmeo  15030  isxmet2d  15059  blin2  15143  comet  15210  metcn  15225  txmetcn  15230  qtopbasss  15232  qtopbas  15233  remetdval  15258  bl2ioo  15261  blssioo  15264  divcnap  15276  cncfmet  15303  dvaddxxbr  15412  dvcjbr  15419  plyf  15448  ply1termlem  15453  plymullem1  15459  plyaddlem  15460  plymullem  15461  plycolemc  15469  plyreres  15475  dvply1  15476  efle  15487  reapef  15489  sinperlem  15519  sincosq2sgn  15538  sincosq3sgn  15539  sincos6thpi  15553  ioocosf1o  15565  relogoprlem  15579  logleb  15586  cxple3  15632  cxpcom  15649  dvdsppwf1o  15700  fsumdvdsmul  15702  1sgmprm  15705  mersenne  15708  lgslem3  15718  lgsdir2  15749  lgsdir  15751  lgsdilem2  15752  lgsdi  15753  gausslemma2dlem1a  15774  gausslemma2dlem3  15779  gausslemma2dlem6  15783  lgseisenlem3  15788  lgseisenlem4  15789  lgsquadlem1  15793  lgsquadlem2  15794  lgsquad2  15799  lgsquad3  15800  2lgslem1a1  15802  2lgslem1a  15804  2lgslem1c  15806  2sqlem2  15831  mul2sq  15832  2sqlem7  15837  usgredg2v  16059  ushgredgedg  16061  ushgredgedgloop  16063  vtxedgfi  16091  vtxlpfi  16092  wlkeq  16142  uspgr2wlkeq  16153  clwwlkccatlem  16185  clwwlkccat  16186  clwwlknccat  16208  bj-inex  16412  bj-bdfindis  16452  triap  16543  cvgcmp2nlemabs  16546  trilpolemisumle  16552  inffz  16586