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  2209  sylan9eq  2246  csbcomg  3103  sylan9ss  3192  ssconb  3292  ineqan12d  3362  dfopg  3802  breqan12d  4045  opexg  4257  copsex2g  4275  ordin  4416  onin  4417  unexg  4474  eusv1  4483  opelvvg  4708  opthprc  4710  opbrop  4738  relop  4812  dmpropg  5138  unixpm  5201  funssres  5296  funinsn  5303  funtp  5307  fnco  5362  resasplitss  5433  fodmrnu  5484  relrnfvex  5572  fconst2g  5773  oveqan12d  5937  ovi3  6055  ovg  6057  f1opw2  6124  off  6143  offres  6187  iunon  6337  nnsucsssuc  6545  nnaword1  6566  ertr  6602  erex  6611  brecop  6679  ecovdi  6700  ecovidi  6701  mapvalg  6712  pmvalg  6713  pmss12g  6729  mapsn  6744  en2sn  6867  xpf1o  6900  xpen  6901  phplem4  6911  ssfilem  6931  diffitest  6943  en1eqsn  7007  sbthlem7  7022  ordiso  7095  updjud  7141  fodju0  7206  finnum  7243  pr2nelem  7251  djucomen  7276  exmidontriimlem1  7281  2onetap  7315  ltsopi  7380  pitric  7381  pitri3or  7382  ltdcpi  7383  mulclpi  7388  addcompig  7389  mulcompig  7391  distrpig  7393  ltexpi  7397  ltapig  7398  ltmpig  7399  dfplpq2  7414  dfmpq2  7415  enqbreq2  7417  enqdc  7421  addcmpblnq  7427  addpipqqslem  7429  mulpipq2  7431  mulpipq  7432  mulpipqqs  7433  addclnq  7435  distrnqg  7447  ltdcnq  7457  ltrnqg  7480  enq0breq  7496  addclnq0  7511  nqnq0a  7514  nqnq0m  7515  nq0m0r  7516  distrnq0  7519  mulcomnq0  7520  genipv  7569  genplt2i  7570  genpelvl  7572  genpelvu  7573  addnqprlemrl  7617  addnqprlemru  7618  addnqprlemfl  7619  addnqprlemfu  7620  addnqpr  7621  mulnqprlemrl  7633  mulnqprlemru  7634  mulnqprlemfl  7635  mulnqprlemfu  7636  mulnqpr  7637  distrlem4prl  7644  distrlem4pru  7645  ltnqpr  7653  recexprlemloc  7691  archrecnq  7723  mulclsr  7814  1idsr  7828  00sr  7829  prsradd  7846  axmulass  7933  axdistr  7934  axcnre  7941  peano5nnnn  7952  mulrid  8016  axltadd  8089  lenlt  8095  cnegexlem3  8196  cnegex  8197  resubcl  8283  subeqrev  8395  muladd  8403  mulsub  8420  mulsub2  8421  ltaddsub2  8456  leaddsub2  8458  leltadd  8466  ltaddpos2  8472  posdif  8474  addge02  8492  mullt0  8499  recexre  8597  recextlem1  8670  recexap  8672  divmuldivap  8731  conjmulap  8748  div2subap  8856  prodgt02  8872  prodge02  8874  lemul2  8876  lemul2a  8878  ltmulgt12  8884  lemulge12  8886  ltmuldiv2  8894  ltdivmul2  8897  ledivmul2  8899  lemuldiv2  8901  negiso  8974  cju  8980  peano5nni  8985  nnaddcl  9002  nnmulcl  9003  nnsub  9021  addltmul  9219  avgle1  9223  avgle2  9224  nnrecl  9238  nn0nnaddcl  9271  zsubcl  9358  zleloe  9364  znnsub  9368  nzadd  9369  zmulcl  9370  zltp1le  9371  zleltp1  9372  nnleltp1  9376  nnltp1le  9377  nnaddm1cl  9378  nn0ltp1le  9379  nn0leltp1  9380  nn0ltlem1  9381  znn0sub  9382  nn0sub  9383  elz2  9388  zapne  9391  zdcle  9393  zdclt  9394  zltlen  9395  nn0lem1lt  9400  nnlem1lt  9401  nnltlem1  9402  zdiv  9405  zextle  9408  zextlt  9409  btwnnz  9411  prime  9416  nneo  9420  peano2uz2  9424  peano5uzti  9425  uzind  9428  fzind  9432  fnn0ind  9433  uzneg  9611  uz11  9615  eluzp1m1  9616  eluzp1p1  9618  uzin  9625  indstr  9658  uz2mulcl  9673  qre  9690  qaddcl  9700  qsubcl  9703  qltlen  9705  qlttri2  9706  irradd  9711  elpqb  9715  cnref1o  9716  rpaddcl  9743  rpmulcl  9744  rpdivcl  9745  rexadd  9918  rexsub  9919  xaddcom  9927  xnn0xadd0  9933  xnegdi  9934  elicc2  10004  iccshftr  10060  iccshftl  10062  iccdil  10064  icccntr  10066  fzval2  10077  elfz1eq  10101  peano2fzr  10103  fznlem  10107  fzsplit2  10116  fzaddel  10125  fzsubel  10126  fzrev2  10151  fzrev3  10153  uzsplit  10158  fzrevral  10171  fzrevral3  10173  fzshftral  10174  elfz2nn0  10178  fznn0sub2  10194  fz0fzdiffz0  10196  elfzmlbp  10198  difelfzle  10200  difelfznle  10201  1fv  10205  elfzouz2  10228  fzouzsplit  10246  elfzo0le  10252  fzonmapblen  10254  fzofzim  10255  fzoaddel2  10260  eluzgtdifelfzo  10264  elfzodifsumelfzo  10268  ubmelm1fzo  10293  fzofzp1b  10295  fzosplitprm1  10301  fzostep1  10304  subfzo0  10309  qdclt  10315  qbtwnxr  10326  flqbi2  10360  divfl0  10365  flqzadd  10367  flqmulnn0  10368  addmodidr  10444  modfzo0difsn  10466  frec2uzltd  10474  frec2uzrand  10476  frecfzen2  10498  seqshft2g  10553  seq3split  10559  seqsplitg  10560  seq3caopr2  10564  seqcaopr2g  10565  seqf1oglem2  10591  exp3vallem  10611  expcllem  10621  expcl2lemap  10622  1exp  10639  expge1  10647  expadd  10652  expmul  10655  expsubap  10658  leexp1a  10665  lt2sq  10684  le2sq  10685  sumsqeq0  10689  qsqeqor  10721  bernneq  10731  bernneq2  10732  sq11ap  10778  facdiv  10809  faclbnd  10812  faclbnd3  10814  faclbnd6  10815  facavg  10817  bcrpcl  10824  bccmpl  10825  fiubm  10899  seq3coll  10913  eqwrd  10954  shftfvalg  10962  shftf  10974  crre  11001  crim  11002  mulreap  11008  readd  11013  resub  11014  remul2  11017  imadd  11021  imsub  11022  immul2  11024  ipcnval  11030  cjsub  11036  cjreim  11047  caucvgre  11125  rexanuz  11132  rexuz3  11134  resqrexlemover  11154  resqrexlemcvg  11163  resqrexlemglsq  11166  sqrtle  11180  sqrtlt  11181  sqrt11ap  11182  sqrt11  11183  absreimsq  11211  absreim  11212  absmul  11213  sqabs  11226  absdiflt  11236  absdifle  11237  abssuble0  11247  abs2difabs  11252  fzomaxdif  11257  caubnd2  11261  rpmaxcl  11367  zmaxcl  11368  minmax  11373  mincl  11374  min1inf  11375  min2inf  11376  minabs  11379  minclpr  11380  rpmincl  11381  2zinfmin  11386  xrmaxrecl  11398  xrminmax  11408  xrmincl  11409  xrmin1inf  11410  xrmin2inf  11411  xrminrecl  11416  xrminrpcl  11417  iooinsup  11420  climconst2  11434  climuni  11436  2clim  11444  climshft  11447  climshft2  11449  cjcn2  11459  climaddc1  11472  climmulc2  11474  climsubc1  11475  climsubc2  11476  climlec2  11484  summodclem2a  11524  zsumdc  11527  isumclim3  11566  mptfzshft  11585  fsumrev  11586  fisum0diag2  11590  telfsumo2  11610  fsumparts  11613  cvgcmpub  11619  binomlem  11626  binom1p  11628  binom1dif  11630  bcxmas  11632  isumshft  11633  expcnvap0  11645  expcnv  11647  geosergap  11649  geolim  11654  cvgratnnlemrate  11673  mertenslemi1  11678  mertenslem2  11679  mertensabs  11680  prodmodc  11721  zproddc  11722  fprodf1o  11731  fprodeq0  11760  efcj  11816  eftlub  11833  effsumlt  11835  efieq  11878  sinsub  11883  cossub  11884  subsin  11886  sinmul  11887  cosmul  11888  addcos  11889  subcos  11890  dvdssub2  11978  dvdsadd  11979  dvdsaddr  11980  dvdssub  11981  dvdssubr  11982  fzocongeq  12000  odd2np1  12014  opoe  12036  omoe  12037  opeo  12038  omeo  12039  divalgb  12066  ndvdsadd  12072  gcdmndc  12081  zsupcllemstep  12082  gcdabs  12125  dvdsgcd  12149  absmulgcd  12154  gcdmultiple  12157  gcdmultiplez  12158  rpmulgcd  12163  sqgcd  12166  dvdssqlem  12167  dvdssq  12168  nninfctlemfo  12177  nn0seqcvgd  12179  ialgrlemconst  12181  algrf  12183  algrp1  12184  algcvg  12186  algcvga  12189  lcmval  12201  lcmabs  12214  lcmgcd  12216  lcmdvds  12217  lcmgcdnn  12220  coprmgcdb  12226  coprmdvds  12230  coprmdvds2  12231  qredeq  12234  isprm3  12256  nprm  12261  divgcdodd  12281  prmdvdsexp  12286  sqrt2irr  12300  zgcdsq  12339  hashdvds  12359  phiprmpw  12360  crth  12362  phimullem  12363  modprm0  12392  coprimeprodsq  12395  coprimeprodsq2  12396  pythagtriplem2  12404  pythagtriplem19  12420  pcdvdsb  12458  pcneg  12463  pc2dvds  12468  pc11  12469  pcmpt  12481  pcfac  12488  infpnlem1  12497  prmunb  12500  1arithlem4  12504  1arith  12505  gzaddcl  12515  gzmulcl  12516  gzreim  12517  gzsubcl  12518  4sqlem1  12526  4sqlem4a  12529  4sqlem4  12530  4sqlem12  12540  setsvalg  12648  setsfun0  12654  restval  12856  xpsval  12935  mndinvmod  13026  resmhm  13059  resmhm2  13060  mhmco  13062  dfgrp3m  13171  mhmmnd  13186  mulgnngsum  13197  mulgnn0z  13219  mulgnndir  13221  ghmex  13325  0ghm  13328  resghm  13330  resghm2  13331  ghmco  13334  ghmeql  13337  kerf1ghm  13344  ablsubsub23  13395  dfrhm2  13650  isrhm  13654  rhmfn  13668  rhmval  13669  rhmco  13670  resrhm  13744  rhmeql  13746  rhmima  13747  lmodfopne  13822  lspf  13885  znidom  14145  znrrg  14148  innei  14331  cnovex  14364  txuni2  14424  txbasex  14425  txbas  14426  txtop  14428  txtopon  14430  txss12  14434  txbasval  14435  txcnp  14439  upxp  14440  txcnmpt  14441  uptx  14442  txcn  14443  txrest  14444  txdis  14445  cnmpt21  14459  hmeoco  14484  txhmeo  14487  isxmet2d  14516  blin2  14600  comet  14667  metcn  14682  txmetcn  14687  qtopbasss  14689  qtopbas  14690  remetdval  14707  bl2ioo  14710  blssioo  14713  divcnap  14723  cncfmet  14747  dvaddxxbr  14850  dvcjbr  14857  plyf  14883  ply1termlem  14888  plymullem1  14894  plyaddlem  14895  plymullem  14896  efle  14911  reapef  14913  sinperlem  14943  sincosq2sgn  14962  sincosq3sgn  14963  sincos6thpi  14977  ioocosf1o  14989  relogoprlem  15003  logleb  15010  cxple3  15055  cxpcom  15071  lgslem3  15118  lgsdir2  15149  lgsdir  15151  lgsdilem2  15152  lgsdi  15153  gausslemma2dlem1a  15174  gausslemma2dlem3  15179  gausslemma2dlem6  15183  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191  2sqlem2  15202  mul2sq  15203  2sqlem7  15208  bj-inex  15399  bj-bdfindis  15439  triap  15519  cvgcmp2nlemabs  15522  trilpolemisumle  15528  inffz  15562