Theorem syl2an 284

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 278	. 2 |- ( ( ph /\ ch ) -> th )
5	1, 4	sylan2 281	1 |- ( ( ph /\ ta ) -> th )

Syntax hints:   -> wi 4   /\ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  syl2anr  285  anim12i  332  syl2an2  562  syl2an2r  563  mp3an3an  1280  eqeqan12d  2104  sylan9eq  2141  csbcomg  2955  sylan9ss  3039  ssconb  3134  ineqan12d  3204  dfopg  3626  breqan12d  3866  opexg  4064  copsex2g  4082  ordin  4221  onin  4222  unexg  4278  eusv1  4287  opelvvg  4500  opthprc  4502  opbrop  4530  relop  4599  dmpropg  4916  unixpm  4979  funssres  5069  funinsn  5076  funtp  5080  fnco  5135  resasplitss  5203  fodmrnu  5254  relrnfvex  5336  fconst2g  5526  oveqan12d  5685  ovi3  5795  ovg  5797  f1opw2  5864  off  5882  offres  5920  iunon  6063  nnsucsssuc  6267  nnaword1  6286  ertr  6321  erex  6330  brecop  6396  ecovdi  6417  ecovidi  6418  mapvalg  6429  pmvalg  6430  pmss12g  6446  mapsn  6461  en2sn  6584  xpf1o  6614  xpen  6615  phplem4  6625  ssfilem  6645  diffitest  6657  en1eqsn  6711  sbthlem7  6726  ordiso  6783  updjud  6827  fodjuomnilem0  6856  finnum  6865  pr2nelem  6873  ltsopi  6933  pitric  6934  pitri3or  6935  ltdcpi  6936  mulclpi  6941  addcompig  6942  mulcompig  6944  distrpig  6946  ltexpi  6950  ltapig  6951  ltmpig  6952  dfplpq2  6967  dfmpq2  6968  enqbreq2  6970  enqdc  6974  addcmpblnq  6980  addpipqqslem  6982  mulpipq2  6984  mulpipq  6985  mulpipqqs  6986  addclnq  6988  distrnqg  7000  ltdcnq  7010  ltrnqg  7033  enq0breq  7049  addclnq0  7064  nqnq0a  7067  nqnq0m  7068  nq0m0r  7069  distrnq0  7072  mulcomnq0  7073  genipv  7122  genplt2i  7123  genpelvl  7125  genpelvu  7126  addnqprlemrl  7170  addnqprlemru  7171  addnqprlemfl  7172  addnqprlemfu  7173  addnqpr  7174  mulnqprlemrl  7186  mulnqprlemru  7187  mulnqprlemfl  7188  mulnqprlemfu  7189  mulnqpr  7190  distrlem4prl  7197  distrlem4pru  7198  ltnqpr  7206  recexprlemloc  7244  archrecnq  7276  mulclsr  7354  1idsr  7368  00sr  7369  prsradd  7385  axmulass  7462  axdistr  7463  axcnre  7470  peano5nnnn  7481  mulid1  7539  axltadd  7610  lenlt  7615  cnegexlem3  7713  cnegex  7714  resubcl  7800  subeqrev  7908  muladd  7916  mulsub  7933  mulsub2  7934  ltaddsub2  7969  leaddsub2  7971  leltadd  7979  ltaddpos2  7985  posdif  7987  addge02  8005  mullt0  8012  recexre  8109  recextlem1  8174  recexap  8176  divmuldivap  8233  conjmulap  8250  div2subap  8356  prodgt02  8368  prodge02  8370  lemul2  8372  lemul2a  8374  ltmulgt12  8380  lemulge12  8382  ltmuldiv2  8390  ltdivmul2  8393  ledivmul2  8395  lemuldiv2  8397  negiso  8470  cju  8475  peano5nni  8479  nnaddcl  8496  nnmulcl  8497  nnsub  8515  addltmul  8706  avgle1  8710  avgle2  8711  nnrecl  8725  nn0nnaddcl  8758  zsubcl  8845  zleloe  8851  znnsub  8855  nzadd  8856  zmulcl  8857  zltp1le  8858  zleltp1  8859  nnleltp1  8863  nnltp1le  8864  nnaddm1cl  8865  nn0ltp1le  8866  nn0leltp1  8867  nn0ltlem1  8868  znn0sub  8869  nn0sub  8870  elz2  8872  zapne  8875  zdcle  8877  zdclt  8878  zltlen  8879  nn0lem1lt  8883  nnlem1lt  8884  nnltlem1  8885  zdiv  8888  zextle  8891  zextlt  8892  btwnnz  8894  prime  8899  nneo  8903  peano2uz2  8907  peano5uzti  8908  uzind  8911  fzind  8915  fnn0ind  8916  uzneg  9091  uz11  9095  eluzp1m1  9096  eluzp1p1  9098  uzin  9105  indstr  9135  uz2mulcl  9149  qre  9164  qaddcl  9174  qsubcl  9177  qltlen  9179  qlttri2  9180  irradd  9185  cnref1o  9187  rpaddcl  9211  rpmulcl  9212  rpdivcl  9213  elicc2  9410  iccshftr  9465  iccshftl  9467  iccdil  9469  icccntr  9471  fzval2  9481  elfz1eq  9503  peano2fzr  9505  fznlem  9509  fzsplit2  9518  fzaddel  9527  fzsubel  9528  fzrev2  9553  fzrev3  9555  uzsplit  9560  fzrevral  9573  fzrevral3  9575  fzshftral  9576  elfz2nn0  9580  fznn0sub2  9593  fz0fzdiffz0  9595  elfzmlbp  9597  difelfzle  9599  difelfznle  9600  1fv  9604  elfzouz2  9626  fzouzsplit  9644  elfzo0le  9650  fzonmapblen  9652  fzofzim  9653  fzoaddel2  9658  eluzgtdifelfzo  9662  elfzodifsumelfzo  9666  ubmelm1fzo  9691  fzofzp1b  9693  fzosplitprm1  9699  fzostep1  9702  subfzo0  9707  qbtwnxr  9723  flqbi2  9752  divfl0  9757  flqzadd  9759  flqmulnn0  9760  addmodidr  9834  modfzo0difsn  9856  frec2uzltd  9864  frec2uzrand  9866  frecfzen2  9888  iseqshft2  9952  seq3split  9961  iseqsplit  9962  iseqcaopr2  9965  exp3vallem  10010  expcllem  10020  expcl2lemap  10021  1exp  10038  expge1  10046  expadd  10051  expmul  10054  expsubap  10057  leexp1a  10064  lt2sq  10082  le2sq  10083  sumsqeq0  10087  bernneq  10128  bernneq2  10129  sq11ap  10174  facdiv  10200  faclbnd  10203  faclbnd3  10205  faclbnd6  10206  facavg  10208  bcrpcl  10215  bccmpl  10216  iseqcoll  10301  shftfvalg  10306  shftf  10318  crre  10345  crim  10346  mulreap  10352  readd  10357  resub  10358  remul2  10361  imadd  10365  imsub  10366  immul2  10368  ipcnval  10374  cjsub  10380  cjreim  10391  caucvgre  10468  rexanuz  10475  rexuz3  10477  resqrexlemover  10497  resqrexlemcvg  10506  resqrexlemglsq  10509  sqrtle  10523  sqrtlt  10524  sqrt11ap  10525  sqrt11  10526  absreimsq  10554  absreim  10555  absmul  10556  sqabs  10569  absdiflt  10579  absdifle  10580  abssuble0  10590  abs2difabs  10595  fzomaxdif  10600  caubnd2  10604  zmaxcl  10710  minmax  10715  min1inf  10716  min2inf  10717  climconst2  10733  climuni  10735  2clim  10743  climshft  10746  climshft2  10749  cjcn2  10758  climaddc1  10771  climmulc2  10773  climsubc1  10774  climsubc2  10775  climlec2  10784  isummolem2a  10825  zisum  10828  isumclim3  10871  mptfzshft  10890  fsumrev  10891  fisum0diag2  10895  telfsumo2  10915  fsumparts  10918  cvgcmpub  10924  binomlem  10931  binom1p  10933  binom1dif  10935  bcxmas  10937  isumshft  10938  expcnvap0  10950  expcnv  10952  geosergap  10954  geolim  10959  cvgratnnlemrate  10978  mertenslemi1  10983  mertenslem2  10984  mertensabs  10985  efcj  11017  eftlub  11034  effsumlt  11036  efieq  11080  sinsub  11085  cossub  11086  subsin  11088  sinmul  11089  cosmul  11090  addcos  11091  subcos  11092  dvdssub2  11170  dvdsadd  11171  dvdsaddr  11172  dvdssub  11173  dvdssubr  11174  fzocongeq  11191  odd2np1  11205  opoe  11227  omoe  11228  opeo  11229  omeo  11230  divalgb  11257  ndvdsadd  11263  zsupcllemstep  11273  gcdabs  11311  dvdsgcd  11333  absmulgcd  11338  gcdmultiple  11341  gcdmultiplez  11342  rpmulgcd  11347  sqgcd  11350  dvdssqlem  11351  dvdssq  11352  nn0seqcvgd  11355  ialgrlemconst  11357  algrf  11359  algrp1  11360  algcvg  11362  algcvga  11365  lcmval  11377  lcmabs  11390  lcmgcd  11392  lcmdvds  11393  lcmgcdnn  11396  coprmgcdb  11402  coprmdvds  11406  coprmdvds2  11407  qredeq  11410  isprm3  11432  nprm  11437  divgcdodd  11454  prmdvdsexp  11459  sqrt2irr  11473  zgcdsq  11511  hashdvds  11529  phiprmpw  11530  crth  11532  phimullem  11533  setsvalg  11578  setsfun0  11584  restval  11712  bj-inex  12064  bj-bdfindis  12108  inffz  12183