MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mp3an13 Structured version   Unicode version

Theorem mp3an13 1316
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
Hypotheses
Ref Expression
mp3an13.1  |-  ph
mp3an13.2  |-  ch
mp3an13.3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an13  |-  ( ps 
->  th )

Proof of Theorem mp3an13
StepHypRef Expression
1 mp3an13.1 . 2  |-  ph
2 mp3an13.2 . . 3  |-  ch
3 mp3an13.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
42, 3mp3an3 1314 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 670 1  |-  ( ps 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 974
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 976
This theorem is referenced by:  oeoalem  7247  mulid1  9596  addltmul  10780  uzindOLD  10963  eluzaddi  11116  fz01en  11722  fznatpl1  11743  expubnd  12205  bernneq  12271  bernneq2  12272  faclbnd4lem1  12350  hashfun  12474  efi4p  13749  efival  13764  cos2tsin  13791  cos01bnd  13798  cos01gt0  13803  dvds0  13876  odd2np1  13923  divalglem0  13928  gcdid  14046  opoe  14212  pythagtriplem4  14220  ressid  14569  zringcyg  18386  zcyg  18391  lecldbas  19593  blssioo  21173  tgioo  21174  rerest  21182  xrrest  21185  zdis  21194  reconnlem2  21205  metdscn2  21234  negcncf  21295  iihalf2  21306  cncmet  21634  rrxmvallem  21704  rrxmval  21705  ovolunlem1a  21780  ismbf3d  21934  c1lip2  22272  pilem2  22719  pilem3  22720  sinperlem  22745  sincosq1sgn  22763  sincosq2sgn  22764  sinq12gt0  22772  cosq14gt0  22775  cosq14ge0  22776  coseq1  22787  sinord  22793  1sgmprm  23346  ppiub  23351  chtublem  23358  chtub  23359  bcp1ctr  23426  bpos1lem  23429  bposlem2  23432  bposlem3  23433  bposlem4  23434  bposlem5  23435  bposlem6  23436  bposlem7  23437  bposlem9  23439  axlowdim  24136  2trllemD  24431  2trllemG  24432  constr1trl  24462  constr3lem4  24519  ipidsq  25495  ipasslem1  25618  ipasslem2  25619  ipasslem4  25621  ipasslem5  25622  ipasslem8  25624  ipasslem9  25625  ipasslem11  25627  pjoc1i  26221  h1de2bi  26344  h1de2ctlem  26345  spanunsni  26369  opsqrlem1  26931  opsqrlem6  26936  chrelati  27155  chrelat2i  27156  cvexchlem  27159  pnfinf  27600  rrhre  27872  zetacvg  28430  erdszelem5  28512  predeq2  29222  wrecseq2  29315  wsuceq2  29347  bpoly2  29794  bpoly3  29795  fsumcube  29797  sin2h  30020  cos2h  30021  tan2h  30022  mblfinlem1  30026  heiborlem6  30287  icccncfext  31597  dirkertrigeq  31772  zlmodzxzel  32677  onetansqsecsq  32890  cotsqcscsq  32891  taupilem1  37436
  Copyright terms: Public domain W3C validator