Theorem syl2an 287

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

Syntax hints:   -> wi 4   /\ wa 103

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

This theorem is referenced by:  syl2anr  288  anim12i  336  syl2an2  589  syl2an2r  590  mp3an3an  1338  eqeqan12d  2186  sylan9eq  2223  csbcomg  3072  sylan9ss  3160  ssconb  3260  ineqan12d  3330  dfopg  3763  breqan12d  4005  opexg  4213  copsex2g  4231  ordin  4370  onin  4371  unexg  4428  eusv1  4437  opelvvg  4660  opthprc  4662  opbrop  4690  relop  4761  dmpropg  5083  unixpm  5146  funssres  5240  funinsn  5247  funtp  5251  fnco  5306  resasplitss  5377  fodmrnu  5428  relrnfvex  5514  fconst2g  5711  oveqan12d  5872  ovi3  5989  ovg  5991  f1opw2  6055  off  6073  offres  6114  iunon  6263  nnsucsssuc  6471  nnaword1  6492  ertr  6528  erex  6537  brecop  6603  ecovdi  6624  ecovidi  6625  mapvalg  6636  pmvalg  6637  pmss12g  6653  mapsn  6668  en2sn  6791  xpf1o  6822  xpen  6823  phplem4  6833  ssfilem  6853  diffitest  6865  en1eqsn  6925  sbthlem7  6940  ordiso  7013  updjud  7059  fodju0  7123  finnum  7160  pr2nelem  7168  djucomen  7193  exmidontriimlem1  7198  ltsopi  7282  pitric  7283  pitri3or  7284  ltdcpi  7285  mulclpi  7290  addcompig  7291  mulcompig  7293  distrpig  7295  ltexpi  7299  ltapig  7300  ltmpig  7301  dfplpq2  7316  dfmpq2  7317  enqbreq2  7319  enqdc  7323  addcmpblnq  7329  addpipqqslem  7331  mulpipq2  7333  mulpipq  7334  mulpipqqs  7335  addclnq  7337  distrnqg  7349  ltdcnq  7359  ltrnqg  7382  enq0breq  7398  addclnq0  7413  nqnq0a  7416  nqnq0m  7417  nq0m0r  7418  distrnq0  7421  mulcomnq0  7422  genipv  7471  genplt2i  7472  genpelvl  7474  genpelvu  7475  addnqprlemrl  7519  addnqprlemru  7520  addnqprlemfl  7521  addnqprlemfu  7522  addnqpr  7523  mulnqprlemrl  7535  mulnqprlemru  7536  mulnqprlemfl  7537  mulnqprlemfu  7538  mulnqpr  7539  distrlem4prl  7546  distrlem4pru  7547  ltnqpr  7555  recexprlemloc  7593  archrecnq  7625  mulclsr  7716  1idsr  7730  00sr  7731  prsradd  7748  axmulass  7835  axdistr  7836  axcnre  7843  peano5nnnn  7854  mulid1  7917  axltadd  7989  lenlt  7995  cnegexlem3  8096  cnegex  8097  resubcl  8183  subeqrev  8295  muladd  8303  mulsub  8320  mulsub2  8321  ltaddsub2  8356  leaddsub2  8358  leltadd  8366  ltaddpos2  8372  posdif  8374  addge02  8392  mullt0  8399  recexre  8497  recextlem1  8569  recexap  8571  divmuldivap  8629  conjmulap  8646  div2subap  8754  prodgt02  8769  prodge02  8771  lemul2  8773  lemul2a  8775  ltmulgt12  8781  lemulge12  8783  ltmuldiv2  8791  ltdivmul2  8794  ledivmul2  8796  lemuldiv2  8798  negiso  8871  cju  8877  peano5nni  8881  nnaddcl  8898  nnmulcl  8899  nnsub  8917  addltmul  9114  avgle1  9118  avgle2  9119  nnrecl  9133  nn0nnaddcl  9166  zsubcl  9253  zleloe  9259  znnsub  9263  nzadd  9264  zmulcl  9265  zltp1le  9266  zleltp1  9267  nnleltp1  9271  nnltp1le  9272  nnaddm1cl  9273  nn0ltp1le  9274  nn0leltp1  9275  nn0ltlem1  9276  znn0sub  9277  nn0sub  9278  elz2  9283  zapne  9286  zdcle  9288  zdclt  9289  zltlen  9290  nn0lem1lt  9295  nnlem1lt  9296  nnltlem1  9297  zdiv  9300  zextle  9303  zextlt  9304  btwnnz  9306  prime  9311  nneo  9315  peano2uz2  9319  peano5uzti  9320  uzind  9323  fzind  9327  fnn0ind  9328  uzneg  9505  uz11  9509  eluzp1m1  9510  eluzp1p1  9512  uzin  9519  indstr  9552  uz2mulcl  9567  qre  9584  qaddcl  9594  qsubcl  9597  qltlen  9599  qlttri2  9600  irradd  9605  elpqb  9608  cnref1o  9609  rpaddcl  9634  rpmulcl  9635  rpdivcl  9636  rexadd  9809  rexsub  9810  xaddcom  9818  xnn0xadd0  9824  xnegdi  9825  elicc2  9895  iccshftr  9951  iccshftl  9953  iccdil  9955  icccntr  9957  fzval2  9968  elfz1eq  9991  peano2fzr  9993  fznlem  9997  fzsplit2  10006  fzaddel  10015  fzsubel  10016  fzrev2  10041  fzrev3  10043  uzsplit  10048  fzrevral  10061  fzrevral3  10063  fzshftral  10064  elfz2nn0  10068  fznn0sub2  10084  fz0fzdiffz0  10086  elfzmlbp  10088  difelfzle  10090  difelfznle  10091  1fv  10095  elfzouz2  10117  fzouzsplit  10135  elfzo0le  10141  fzonmapblen  10143  fzofzim  10144  fzoaddel2  10149  eluzgtdifelfzo  10153  elfzodifsumelfzo  10157  ubmelm1fzo  10182  fzofzp1b  10184  fzosplitprm1  10190  fzostep1  10193  subfzo0  10198  qbtwnxr  10214  flqbi2  10247  divfl0  10252  flqzadd  10254  flqmulnn0  10255  addmodidr  10329  modfzo0difsn  10351  frec2uzltd  10359  frec2uzrand  10361  frecfzen2  10383  seq3split  10435  seq3caopr2  10438  exp3vallem  10477  expcllem  10487  expcl2lemap  10488  1exp  10505  expge1  10513  expadd  10518  expmul  10521  expsubap  10524  leexp1a  10531  lt2sq  10549  le2sq  10550  sumsqeq0  10554  qsqeqor  10586  bernneq  10596  bernneq2  10597  sq11ap  10643  facdiv  10672  faclbnd  10675  faclbnd3  10677  faclbnd6  10678  facavg  10680  bcrpcl  10687  bccmpl  10688  fiubm  10763  seq3coll  10777  shftfvalg  10782  shftf  10794  crre  10821  crim  10822  mulreap  10828  readd  10833  resub  10834  remul2  10837  imadd  10841  imsub  10842  immul2  10844  ipcnval  10850  cjsub  10856  cjreim  10867  caucvgre  10945  rexanuz  10952  rexuz3  10954  resqrexlemover  10974  resqrexlemcvg  10983  resqrexlemglsq  10986  sqrtle  11000  sqrtlt  11001  sqrt11ap  11002  sqrt11  11003  absreimsq  11031  absreim  11032  absmul  11033  sqabs  11046  absdiflt  11056  absdifle  11057  abssuble0  11067  abs2difabs  11072  fzomaxdif  11077  caubnd2  11081  rpmaxcl  11187  zmaxcl  11188  minmax  11193  mincl  11194  min1inf  11195  min2inf  11196  minabs  11199  minclpr  11200  rpmincl  11201  2zinfmin  11206  xrmaxrecl  11218  xrminmax  11228  xrmincl  11229  xrmin1inf  11230  xrmin2inf  11231  xrminrecl  11236  xrminrpcl  11237  iooinsup  11240  climconst2  11254  climuni  11256  2clim  11264  climshft  11267  climshft2  11269  cjcn2  11279  climaddc1  11292  climmulc2  11294  climsubc1  11295  climsubc2  11296  climlec2  11304  summodclem2a  11344  zsumdc  11347  isumclim3  11386  mptfzshft  11405  fsumrev  11406  fisum0diag2  11410  telfsumo2  11430  fsumparts  11433  cvgcmpub  11439  binomlem  11446  binom1p  11448  binom1dif  11450  bcxmas  11452  isumshft  11453  expcnvap0  11465  expcnv  11467  geosergap  11469  geolim  11474  cvgratnnlemrate  11493  mertenslemi1  11498  mertenslem2  11499  mertensabs  11500  prodmodc  11541  zproddc  11542  fprodf1o  11551  fprodeq0  11580  efcj  11636  eftlub  11653  effsumlt  11655  efieq  11698  sinsub  11703  cossub  11704  subsin  11706  sinmul  11707  cosmul  11708  addcos  11709  subcos  11710  dvdssub2  11797  dvdsadd  11798  dvdsaddr  11799  dvdssub  11800  dvdssubr  11801  fzocongeq  11818  odd2np1  11832  opoe  11854  omoe  11855  opeo  11856  omeo  11857  divalgb  11884  ndvdsadd  11890  zsupcllemstep  11900  gcdabs  11943  dvdsgcd  11967  absmulgcd  11972  gcdmultiple  11975  gcdmultiplez  11976  rpmulgcd  11981  sqgcd  11984  dvdssqlem  11985  dvdssq  11986  nn0seqcvgd  11995  ialgrlemconst  11997  algrf  11999  algrp1  12000  algcvg  12002  algcvga  12005  lcmval  12017  lcmabs  12030  lcmgcd  12032  lcmdvds  12033  lcmgcdnn  12036  coprmgcdb  12042  coprmdvds  12046  coprmdvds2  12047  qredeq  12050  isprm3  12072  nprm  12077  divgcdodd  12097  prmdvdsexp  12102  sqrt2irr  12116  zgcdsq  12155  hashdvds  12175  phiprmpw  12176  crth  12178  phimullem  12179  modprm0  12208  coprimeprodsq  12211  coprimeprodsq2  12212  pythagtriplem2  12220  pythagtriplem19  12236  pcdvdsb  12273  pcneg  12278  pc2dvds  12283  pc11  12284  pcmpt  12295  pcfac  12302  infpnlem1  12311  prmunb  12314  1arithlem4  12318  1arith  12319  gzaddcl  12329  gzmulcl  12330  gzreim  12331  gzsubcl  12332  4sqlem1  12340  4sqlem4a  12343  4sqlem4  12344  setsvalg  12446  setsfun0  12452  restval  12585  mndinvmod  12678  mhmco  12705  innei  12957  cnovex  12990  txuni2  13050  txbasex  13051  txbas  13052  txtop  13054  txtopon  13056  txss12  13060  txbasval  13061  txcnp  13065  upxp  13066  txcnmpt  13067  uptx  13068  txcn  13069  txrest  13070  txdis  13071  cnmpt21  13085  hmeoco  13110  txhmeo  13113  isxmet2d  13142  blin2  13226  comet  13293  metcn  13308  txmetcn  13313  qtopbasss  13315  qtopbas  13316  remetdval  13333  bl2ioo  13336  blssioo  13339  divcnap  13349  cncfmet  13373  dvaddxxbr  13459  dvcjbr  13466  efle  13491  reapef  13493  sinperlem  13523  sincosq2sgn  13542  sincosq3sgn  13543  sincos6thpi  13557  ioocosf1o  13569  relogoprlem  13583  logleb  13590  cxple3  13635  cxpcom  13651  lgslem3  13697  lgsdir2  13728  lgsdir  13730  lgsdilem2  13731  lgsdi  13732  2sqlem2  13745  mul2sq  13746  2sqlem7  13751  bj-inex  13942  bj-bdfindis  13982  triap  14061  cvgcmp2nlemabs  14064  trilpolemisumle  14070  inffz  14101