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  942  mp3an3an  1356  eqeqan12d  2222  sylan9eq  2259  csbcomg  3118  sylan9ss  3208  ssconb  3308  ineqan12d  3378  dfopg  3820  breqan12d  4064  opexg  4277  copsex2g  4295  ordin  4437  onin  4438  unexg  4495  eusv1  4504  opelvvg  4729  opthprc  4731  opbrop  4759  relop  4833  dmpropg  5161  unixpm  5224  funssres  5319  funinsn  5329  funtp  5333  fnco  5390  resasplitss  5464  fodmrnu  5515  relrnfvex  5604  funopdmsn  5774  fconst2g  5809  oveqan12d  5973  ovi3  6093  ovg  6095  f1opw2  6162  off  6181  offres  6230  iunon  6380  nnsucsssuc  6588  nnaword1  6609  ertr  6645  erex  6654  brecop  6722  ecovdi  6743  ecovidi  6744  mapvalg  6755  pmvalg  6756  pmss12g  6772  mapsn  6787  en2sn  6916  xpf1o  6953  xpen  6954  phplem4  6964  ssfilem  6984  diffitest  6996  en1eqsn  7062  sbthlem7  7077  ordiso  7150  updjud  7196  fodju0  7261  finnum  7302  pr2nelem  7311  djucomen  7341  exmidontriimlem1  7346  2onetap  7380  ltsopi  7446  pitric  7447  pitri3or  7448  ltdcpi  7449  mulclpi  7454  addcompig  7455  mulcompig  7457  distrpig  7459  ltexpi  7463  ltapig  7464  ltmpig  7465  dfplpq2  7480  dfmpq2  7481  enqbreq2  7483  enqdc  7487  addcmpblnq  7493  addpipqqslem  7495  mulpipq2  7497  mulpipq  7498  mulpipqqs  7499  addclnq  7501  distrnqg  7513  ltdcnq  7523  ltrnqg  7546  enq0breq  7562  addclnq0  7577  nqnq0a  7580  nqnq0m  7581  nq0m0r  7582  distrnq0  7585  mulcomnq0  7586  genipv  7635  genplt2i  7636  genpelvl  7638  genpelvu  7639  addnqprlemrl  7683  addnqprlemru  7684  addnqprlemfl  7685  addnqprlemfu  7686  addnqpr  7687  mulnqprlemrl  7699  mulnqprlemru  7700  mulnqprlemfl  7701  mulnqprlemfu  7702  mulnqpr  7703  distrlem4prl  7710  distrlem4pru  7711  ltnqpr  7719  recexprlemloc  7757  archrecnq  7789  mulclsr  7880  1idsr  7894  00sr  7895  prsradd  7912  axmulass  7999  axdistr  8000  axcnre  8007  peano5nnnn  8018  mulrid  8082  axltadd  8155  lenlt  8161  cnegexlem3  8262  cnegex  8263  resubcl  8349  subeqrev  8461  muladd  8469  mulsub  8486  mulsub2  8487  ltaddsub2  8523  leaddsub2  8525  leltadd  8533  ltaddpos2  8539  posdif  8541  addge02  8559  mullt0  8566  recexre  8664  recextlem1  8737  recexap  8739  divmuldivap  8798  conjmulap  8815  div2subap  8923  prodgt02  8939  prodge02  8941  lemul2  8943  lemul2a  8945  ltmulgt12  8951  lemulge12  8953  ltmuldiv2  8961  ltdivmul2  8964  ledivmul2  8966  lemuldiv2  8968  negiso  9041  cju  9047  peano5nni  9052  nnaddcl  9069  nnmulcl  9070  nnsub  9088  addltmul  9287  avgle1  9291  avgle2  9292  nnrecl  9306  nn0nnaddcl  9339  zsubcl  9426  zleloe  9432  znnsub  9437  nzadd  9438  zmulcl  9439  zltp1le  9440  zleltp1  9441  nnleltp1  9445  nnltp1le  9446  nnaddm1cl  9447  nn0ltp1le  9448  nn0leltp1  9449  nn0ltlem1  9450  znn0sub  9451  nn0sub  9452  elz2  9457  zapne  9460  zdcle  9462  zdclt  9463  zltlen  9464  nn0lem1lt  9469  nnlem1lt  9470  nnltlem1  9471  zdiv  9474  zextle  9477  zextlt  9478  btwnnz  9480  prime  9485  nneo  9489  peano2uz2  9493  peano5uzti  9494  uzind  9497  fzind  9501  fnn0ind  9502  uzneg  9680  uz11  9684  eluzp1m1  9685  eluzp1p1  9687  uzin  9694  indstr  9727  uz2mulcl  9742  qre  9759  qaddcl  9769  qsubcl  9772  qltlen  9774  qlttri2  9775  irradd  9780  elpqb  9784  cnref1o  9785  rpaddcl  9812  rpmulcl  9813  rpdivcl  9814  rexadd  9987  rexsub  9988  xaddcom  9996  xnn0xadd0  10002  xnegdi  10003  elicc2  10073  iccshftr  10129  iccshftl  10131  iccdil  10133  icccntr  10135  fzval2  10146  elfz1eq  10170  peano2fzr  10172  fznlem  10176  fzsplit2  10185  fzaddel  10194  fzsubel  10195  fzrev2  10220  fzrev3  10222  uzsplit  10227  fzrevral  10240  fzrevral3  10242  fzshftral  10243  elfz2nn0  10247  fznn0sub2  10263  fz0fzdiffz0  10265  elfzmlbp  10267  difelfzle  10269  difelfznle  10270  1fv  10274  elfzouz2  10297  fzo0n  10303  fzouzsplit  10316  elfzo0le  10322  fzonmapblen  10324  fzofzim  10325  fzoaddel2  10332  eluzgtdifelfzo  10339  elfzodifsumelfzo  10343  ubmelm1fzo  10368  fzofzp1b  10370  fzosplitprm1  10376  fzostep1  10379  subfzo0  10384  zsupcllemstep  10385  qdclt  10401  qbtwnxr  10413  flqbi2  10447  divfl0  10452  flqzadd  10454  flqmulnn0  10455  addmodidr  10531  modfzo0difsn  10553  frec2uzltd  10561  frec2uzrand  10563  frecfzen2  10585  seqshft2g  10640  seq3split  10646  seqsplitg  10647  seq3caopr2  10651  seqcaopr2g  10652  seqf1oglem2  10678  exp3vallem  10698  expcllem  10708  expcl2lemap  10709  1exp  10726  expge1  10734  expadd  10739  expmul  10742  expsubap  10745  leexp1a  10752  lt2sq  10771  le2sq  10772  sumsqeq0  10776  qsqeqor  10808  bernneq  10818  bernneq2  10819  sq11ap  10865  facdiv  10896  faclbnd  10899  faclbnd3  10901  faclbnd6  10902  facavg  10904  bcrpcl  10911  bccmpl  10912  fiubm  10986  seq3coll  11000  eqwrd  11047  ccatcl  11063  ccatclab  11064  ccatlen  11065  ccat0  11066  ccatval1  11067  ccatval2  11068  elfzelfzccat  11070  ccatvalfn  11071  ccatsymb  11072  ccatval21sw  11075  ccatrn  11079  lswccatn0lsw  11081  swrdfv2  11130  swrdsbslen  11133  swrdspsleq  11134  swrdccat2  11138  ccatpfx  11166  pfxccat1  11167  swrdswrdlem  11169  pfxswrd  11171  shftfvalg  11179  shftf  11191  crre  11218  crim  11219  mulreap  11225  readd  11230  resub  11231  remul2  11234  imadd  11238  imsub  11239  immul2  11241  ipcnval  11247  cjsub  11253  cjreim  11264  caucvgre  11342  rexanuz  11349  rexuz3  11351  resqrexlemover  11371  resqrexlemcvg  11380  resqrexlemglsq  11383  sqrtle  11397  sqrtlt  11398  sqrt11ap  11399  sqrt11  11400  absreimsq  11428  absreim  11429  absmul  11430  sqabs  11443  absdiflt  11453  absdifle  11454  abssuble0  11464  abs2difabs  11469  fzomaxdif  11474  caubnd2  11478  rpmaxcl  11584  zmaxcl  11585  nn0maxcl  11586  minmax  11591  mincl  11592  min1inf  11593  min2inf  11594  minabs  11597  minclpr  11598  rpmincl  11599  2zinfmin  11604  xrmaxrecl  11616  xrminmax  11626  xrmincl  11627  xrmin1inf  11628  xrmin2inf  11629  xrminrecl  11634  xrminrpcl  11635  iooinsup  11638  climconst2  11652  climuni  11654  2clim  11662  climshft  11665  climshft2  11667  cjcn2  11677  climaddc1  11690  climmulc2  11692  climsubc1  11693  climsubc2  11694  climlec2  11702  summodclem2a  11742  zsumdc  11745  isumclim3  11784  mptfzshft  11803  fsumrev  11804  fisum0diag2  11808  telfsumo2  11828  fsumparts  11831  cvgcmpub  11837  binomlem  11844  binom1p  11846  binom1dif  11848  bcxmas  11850  isumshft  11851  expcnvap0  11863  expcnv  11865  geosergap  11867  geolim  11872  cvgratnnlemrate  11891  mertenslemi1  11896  mertenslem2  11897  mertensabs  11898  prodmodc  11939  zproddc  11940  fprodf1o  11949  fprodeq0  11978  efcj  12034  eftlub  12051  effsumlt  12053  efieq  12096  sinsub  12101  cossub  12102  subsin  12104  sinmul  12105  cosmul  12106  addcos  12107  subcos  12108  dvdssub2  12196  dvdsadd  12197  dvdsaddr  12198  dvdssub  12199  dvdssubr  12200  fzocongeq  12219  odd2np1  12234  opoe  12256  omoe  12257  opeo  12258  omeo  12259  divalgb  12286  ndvdsadd  12292  bitsfi  12318  gcdmndc  12326  gcdabs  12359  dvdsgcd  12383  absmulgcd  12388  gcdmultiple  12391  gcdmultiplez  12392  rpmulgcd  12397  sqgcd  12400  dvdssqlem  12401  dvdssq  12402  nninfctlemfo  12411  nn0seqcvgd  12413  ialgrlemconst  12415  algrf  12417  algrp1  12418  algcvg  12420  algcvga  12423  lcmval  12435  lcmabs  12448  lcmgcd  12450  lcmdvds  12451  lcmgcdnn  12454  coprmgcdb  12460  coprmdvds  12464  coprmdvds2  12465  qredeq  12468  isprm3  12490  nprm  12495  divgcdodd  12515  prmdvdsexp  12520  sqrt2irr  12534  zgcdsq  12573  hashdvds  12593  phiprmpw  12594  crth  12596  phimullem  12597  modprm0  12627  coprimeprodsq  12630  coprimeprodsq2  12631  pythagtriplem2  12639  pythagtriplem19  12655  pcdvdsb  12693  pcneg  12698  pc2dvds  12703  pc11  12704  pcmpt  12716  pcfac  12723  infpnlem1  12732  prmunb  12735  1arithlem4  12739  1arith  12740  gzaddcl  12750  gzmulcl  12751  gzreim  12752  gzsubcl  12753  4sqlem1  12761  4sqlem4a  12764  4sqlem4  12765  4sqlem12  12775  setsvalg  12912  setsfun0  12918  restval  13127  xpsval  13234  mndinvmod  13327  resmhm  13369  resmhm2  13370  mhmco  13372  dfgrp3m  13481  mhmmnd  13502  mulgnngsum  13513  mulgnn0z  13535  mulgnndir  13537  ghmex  13641  0ghm  13644  resghm  13646  resghm2  13647  ghmco  13650  ghmeql  13653  kerf1ghm  13660  ablsubsub23  13711  dfrhm2  13966  isrhm  13970  rhmfn  13984  rhmval  13985  rhmco  13986  resrhm  14060  rhmeql  14062  rhmima  14063  lmodfopne  14138  lspf  14201  znidom  14469  znrrg  14472  innei  14685  cnovex  14718  txuni2  14778  txbasex  14779  txbas  14780  txtop  14782  txtopon  14784  txss12  14788  txbasval  14789  txcnp  14793  upxp  14794  txcnmpt  14795  uptx  14796  txcn  14797  txrest  14798  txdis  14799  cnmpt21  14813  hmeoco  14838  txhmeo  14841  isxmet2d  14870  blin2  14954  comet  15021  metcn  15036  txmetcn  15041  qtopbasss  15043  qtopbas  15044  remetdval  15069  bl2ioo  15072  blssioo  15075  divcnap  15087  cncfmet  15114  dvaddxxbr  15223  dvcjbr  15230  plyf  15259  ply1termlem  15264  plymullem1  15270  plyaddlem  15271  plymullem  15272  plycolemc  15280  plyreres  15286  dvply1  15287  efle  15298  reapef  15300  sinperlem  15330  sincosq2sgn  15349  sincosq3sgn  15350  sincos6thpi  15364  ioocosf1o  15376  relogoprlem  15390  logleb  15397  cxple3  15443  cxpcom  15460  dvdsppwf1o  15511  fsumdvdsmul  15513  1sgmprm  15516  mersenne  15519  lgslem3  15529  lgsdir2  15560  lgsdir  15562  lgsdilem2  15563  lgsdi  15564  gausslemma2dlem1a  15585  gausslemma2dlem3  15590  gausslemma2dlem6  15594  lgseisenlem3  15599  lgseisenlem4  15600  lgsquadlem1  15604  lgsquadlem2  15605  lgsquad2  15610  lgsquad3  15611  2lgslem1a1  15613  2lgslem1a  15615  2lgslem1c  15617  2sqlem2  15642  mul2sq  15643  2sqlem7  15648  bj-inex  15957  bj-bdfindis  15997  triap  16083  cvgcmp2nlemabs  16086  trilpolemisumle  16092  inffz  16126