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  594  syl2an2r  595  orandc  941  mp3an3an  1354  eqeqan12d  2212  sylan9eq  2249  csbcomg  3107  sylan9ss  3197  ssconb  3297  ineqan12d  3367  dfopg  3807  breqan12d  4050  opexg  4262  copsex2g  4280  ordin  4421  onin  4422  unexg  4479  eusv1  4488  opelvvg  4713  opthprc  4715  opbrop  4743  relop  4817  dmpropg  5143  unixpm  5206  funssres  5301  funinsn  5308  funtp  5312  fnco  5369  resasplitss  5440  fodmrnu  5491  relrnfvex  5579  fconst2g  5780  oveqan12d  5944  ovi3  6064  ovg  6066  f1opw2  6133  off  6152  offres  6201  iunon  6351  nnsucsssuc  6559  nnaword1  6580  ertr  6616  erex  6625  brecop  6693  ecovdi  6714  ecovidi  6715  mapvalg  6726  pmvalg  6727  pmss12g  6743  mapsn  6758  en2sn  6881  xpf1o  6914  xpen  6915  phplem4  6925  ssfilem  6945  diffitest  6957  en1eqsn  7023  sbthlem7  7038  ordiso  7111  updjud  7157  fodju0  7222  finnum  7261  pr2nelem  7270  djucomen  7299  exmidontriimlem1  7304  2onetap  7338  ltsopi  7404  pitric  7405  pitri3or  7406  ltdcpi  7407  mulclpi  7412  addcompig  7413  mulcompig  7415  distrpig  7417  ltexpi  7421  ltapig  7422  ltmpig  7423  dfplpq2  7438  dfmpq2  7439  enqbreq2  7441  enqdc  7445  addcmpblnq  7451  addpipqqslem  7453  mulpipq2  7455  mulpipq  7456  mulpipqqs  7457  addclnq  7459  distrnqg  7471  ltdcnq  7481  ltrnqg  7504  enq0breq  7520  addclnq0  7535  nqnq0a  7538  nqnq0m  7539  nq0m0r  7540  distrnq0  7543  mulcomnq0  7544  genipv  7593  genplt2i  7594  genpelvl  7596  genpelvu  7597  addnqprlemrl  7641  addnqprlemru  7642  addnqprlemfl  7643  addnqprlemfu  7644  addnqpr  7645  mulnqprlemrl  7657  mulnqprlemru  7658  mulnqprlemfl  7659  mulnqprlemfu  7660  mulnqpr  7661  distrlem4prl  7668  distrlem4pru  7669  ltnqpr  7677  recexprlemloc  7715  archrecnq  7747  mulclsr  7838  1idsr  7852  00sr  7853  prsradd  7870  axmulass  7957  axdistr  7958  axcnre  7965  peano5nnnn  7976  mulrid  8040  axltadd  8113  lenlt  8119  cnegexlem3  8220  cnegex  8221  resubcl  8307  subeqrev  8419  muladd  8427  mulsub  8444  mulsub2  8445  ltaddsub2  8481  leaddsub2  8483  leltadd  8491  ltaddpos2  8497  posdif  8499  addge02  8517  mullt0  8524  recexre  8622  recextlem1  8695  recexap  8697  divmuldivap  8756  conjmulap  8773  div2subap  8881  prodgt02  8897  prodge02  8899  lemul2  8901  lemul2a  8903  ltmulgt12  8909  lemulge12  8911  ltmuldiv2  8919  ltdivmul2  8922  ledivmul2  8924  lemuldiv2  8926  negiso  8999  cju  9005  peano5nni  9010  nnaddcl  9027  nnmulcl  9028  nnsub  9046  addltmul  9245  avgle1  9249  avgle2  9250  nnrecl  9264  nn0nnaddcl  9297  zsubcl  9384  zleloe  9390  znnsub  9394  nzadd  9395  zmulcl  9396  zltp1le  9397  zleltp1  9398  nnleltp1  9402  nnltp1le  9403  nnaddm1cl  9404  nn0ltp1le  9405  nn0leltp1  9406  nn0ltlem1  9407  znn0sub  9408  nn0sub  9409  elz2  9414  zapne  9417  zdcle  9419  zdclt  9420  zltlen  9421  nn0lem1lt  9426  nnlem1lt  9427  nnltlem1  9428  zdiv  9431  zextle  9434  zextlt  9435  btwnnz  9437  prime  9442  nneo  9446  peano2uz2  9450  peano5uzti  9451  uzind  9454  fzind  9458  fnn0ind  9459  uzneg  9637  uz11  9641  eluzp1m1  9642  eluzp1p1  9644  uzin  9651  indstr  9684  uz2mulcl  9699  qre  9716  qaddcl  9726  qsubcl  9729  qltlen  9731  qlttri2  9732  irradd  9737  elpqb  9741  cnref1o  9742  rpaddcl  9769  rpmulcl  9770  rpdivcl  9771  rexadd  9944  rexsub  9945  xaddcom  9953  xnn0xadd0  9959  xnegdi  9960  elicc2  10030  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  fzval2  10103  elfz1eq  10127  peano2fzr  10129  fznlem  10133  fzsplit2  10142  fzaddel  10151  fzsubel  10152  fzrev2  10177  fzrev3  10179  uzsplit  10184  fzrevral  10197  fzrevral3  10199  fzshftral  10200  elfz2nn0  10204  fznn0sub2  10220  fz0fzdiffz0  10222  elfzmlbp  10224  difelfzle  10226  difelfznle  10227  1fv  10231  elfzouz2  10254  fzouzsplit  10272  elfzo0le  10278  fzonmapblen  10280  fzofzim  10281  fzoaddel2  10286  eluzgtdifelfzo  10290  elfzodifsumelfzo  10294  ubmelm1fzo  10319  fzofzp1b  10321  fzosplitprm1  10327  fzostep1  10330  subfzo0  10335  zsupcllemstep  10336  qdclt  10352  qbtwnxr  10364  flqbi2  10398  divfl0  10403  flqzadd  10405  flqmulnn0  10406  addmodidr  10482  modfzo0difsn  10504  frec2uzltd  10512  frec2uzrand  10514  frecfzen2  10536  seqshft2g  10591  seq3split  10597  seqsplitg  10598  seq3caopr2  10602  seqcaopr2g  10603  seqf1oglem2  10629  exp3vallem  10649  expcllem  10659  expcl2lemap  10660  1exp  10677  expge1  10685  expadd  10690  expmul  10693  expsubap  10696  leexp1a  10703  lt2sq  10722  le2sq  10723  sumsqeq0  10727  qsqeqor  10759  bernneq  10769  bernneq2  10770  sq11ap  10816  facdiv  10847  faclbnd  10850  faclbnd3  10852  faclbnd6  10853  facavg  10855  bcrpcl  10862  bccmpl  10863  fiubm  10937  seq3coll  10951  eqwrd  10992  shftfvalg  11000  shftf  11012  crre  11039  crim  11040  mulreap  11046  readd  11051  resub  11052  remul2  11055  imadd  11059  imsub  11060  immul2  11062  ipcnval  11068  cjsub  11074  cjreim  11085  caucvgre  11163  rexanuz  11170  rexuz3  11172  resqrexlemover  11192  resqrexlemcvg  11201  resqrexlemglsq  11204  sqrtle  11218  sqrtlt  11219  sqrt11ap  11220  sqrt11  11221  absreimsq  11249  absreim  11250  absmul  11251  sqabs  11264  absdiflt  11274  absdifle  11275  abssuble0  11285  abs2difabs  11290  fzomaxdif  11295  caubnd2  11299  rpmaxcl  11405  zmaxcl  11406  nn0maxcl  11407  minmax  11412  mincl  11413  min1inf  11414  min2inf  11415  minabs  11418  minclpr  11419  rpmincl  11420  2zinfmin  11425  xrmaxrecl  11437  xrminmax  11447  xrmincl  11448  xrmin1inf  11449  xrmin2inf  11450  xrminrecl  11455  xrminrpcl  11456  iooinsup  11459  climconst2  11473  climuni  11475  2clim  11483  climshft  11486  climshft2  11488  cjcn2  11498  climaddc1  11511  climmulc2  11513  climsubc1  11514  climsubc2  11515  climlec2  11523  summodclem2a  11563  zsumdc  11566  isumclim3  11605  mptfzshft  11624  fsumrev  11625  fisum0diag2  11629  telfsumo2  11649  fsumparts  11652  cvgcmpub  11658  binomlem  11665  binom1p  11667  binom1dif  11669  bcxmas  11671  isumshft  11672  expcnvap0  11684  expcnv  11686  geosergap  11688  geolim  11693  cvgratnnlemrate  11712  mertenslemi1  11717  mertenslem2  11718  mertensabs  11719  prodmodc  11760  zproddc  11761  fprodf1o  11770  fprodeq0  11799  efcj  11855  eftlub  11872  effsumlt  11874  efieq  11917  sinsub  11922  cossub  11923  subsin  11925  sinmul  11926  cosmul  11927  addcos  11928  subcos  11929  dvdssub2  12017  dvdsadd  12018  dvdsaddr  12019  dvdssub  12020  dvdssubr  12021  fzocongeq  12040  odd2np1  12055  opoe  12077  omoe  12078  opeo  12079  omeo  12080  divalgb  12107  ndvdsadd  12113  bitsfi  12139  gcdmndc  12147  gcdabs  12180  dvdsgcd  12204  absmulgcd  12209  gcdmultiple  12212  gcdmultiplez  12213  rpmulgcd  12218  sqgcd  12221  dvdssqlem  12222  dvdssq  12223  nninfctlemfo  12232  nn0seqcvgd  12234  ialgrlemconst  12236  algrf  12238  algrp1  12239  algcvg  12241  algcvga  12244  lcmval  12256  lcmabs  12269  lcmgcd  12271  lcmdvds  12272  lcmgcdnn  12275  coprmgcdb  12281  coprmdvds  12285  coprmdvds2  12286  qredeq  12289  isprm3  12311  nprm  12316  divgcdodd  12336  prmdvdsexp  12341  sqrt2irr  12355  zgcdsq  12394  hashdvds  12414  phiprmpw  12415  crth  12417  phimullem  12418  modprm0  12448  coprimeprodsq  12451  coprimeprodsq2  12452  pythagtriplem2  12460  pythagtriplem19  12476  pcdvdsb  12514  pcneg  12519  pc2dvds  12524  pc11  12525  pcmpt  12537  pcfac  12544  infpnlem1  12553  prmunb  12556  1arithlem4  12560  1arith  12561  gzaddcl  12571  gzmulcl  12572  gzreim  12573  gzsubcl  12574  4sqlem1  12582  4sqlem4a  12585  4sqlem4  12586  4sqlem12  12596  setsvalg  12733  setsfun0  12739  restval  12947  xpsval  13054  mndinvmod  13147  resmhm  13189  resmhm2  13190  mhmco  13192  dfgrp3m  13301  mhmmnd  13322  mulgnngsum  13333  mulgnn0z  13355  mulgnndir  13357  ghmex  13461  0ghm  13464  resghm  13466  resghm2  13467  ghmco  13470  ghmeql  13473  kerf1ghm  13480  ablsubsub23  13531  dfrhm2  13786  isrhm  13790  rhmfn  13804  rhmval  13805  rhmco  13806  resrhm  13880  rhmeql  13882  rhmima  13883  lmodfopne  13958  lspf  14021  znidom  14289  znrrg  14292  innei  14483  cnovex  14516  txuni2  14576  txbasex  14577  txbas  14578  txtop  14580  txtopon  14582  txss12  14586  txbasval  14587  txcnp  14591  upxp  14592  txcnmpt  14593  uptx  14594  txcn  14595  txrest  14596  txdis  14597  cnmpt21  14611  hmeoco  14636  txhmeo  14639  isxmet2d  14668  blin2  14752  comet  14819  metcn  14834  txmetcn  14839  qtopbasss  14841  qtopbas  14842  remetdval  14867  bl2ioo  14870  blssioo  14873  divcnap  14885  cncfmet  14912  dvaddxxbr  15021  dvcjbr  15028  plyf  15057  ply1termlem  15062  plymullem1  15068  plyaddlem  15069  plymullem  15070  plycolemc  15078  plyreres  15084  dvply1  15085  efle  15096  reapef  15098  sinperlem  15128  sincosq2sgn  15147  sincosq3sgn  15148  sincos6thpi  15162  ioocosf1o  15174  relogoprlem  15188  logleb  15195  cxple3  15241  cxpcom  15258  dvdsppwf1o  15309  fsumdvdsmul  15311  1sgmprm  15314  mersenne  15317  lgslem3  15327  lgsdir2  15358  lgsdir  15360  lgsdilem2  15361  lgsdi  15362  gausslemma2dlem1a  15383  gausslemma2dlem3  15388  gausslemma2dlem6  15392  lgseisenlem3  15397  lgseisenlem4  15398  lgsquadlem1  15402  lgsquadlem2  15403  lgsquad2  15408  lgsquad3  15409  2lgslem1a1  15411  2lgslem1a  15413  2lgslem1c  15415  2sqlem2  15440  mul2sq  15441  2sqlem7  15446  bj-inex  15637  bj-bdfindis  15677  triap  15760  cvgcmp2nlemabs  15763  trilpolemisumle  15769  inffz  15803