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

Theorem mp3an13 1268
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 1266 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 651 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 934
This theorem is referenced by:  oeoalem  6610  mulid1  8851  addltmul  9963  uzindOLD  10122  eluzaddi  10270  fz01en  10834  expubnd  11178  bernneq  11243  bernneq2  11244  faclbnd4lem1  11322  hashfun  11405  efi4p  12433  efival  12448  cos2tsin  12475  cos01bnd  12482  cos01gt0  12487  dvds0  12560  odd2np1  12603  divalglem0  12608  gcdid  12726  opoe  12880  pythagtriplem4  12888  ressid  13219  zcyg  16461  lecldbas  16965  blssioo  18317  tgioo  18318  rerest  18326  xrrest  18329  zdis  18338  reconnlem2  18348  metdscn2  18377  negcncf  18437  iihalf2  18447  cncmet  18760  ovolunlem1a  18871  ismbf3d  19025  c1lip2  19361  pilem2  19844  pilem3  19845  sinperlem  19864  sincosq1sgn  19882  sincosq2sgn  19883  sinq12gt0  19891  cosq14gt0  19894  cosq14ge0  19895  coseq1  19906  sinord  19912  1sgmprm  20454  ppiub  20459  chtublem  20466  chtub  20467  bcp1ctr  20534  bpos1lem  20537  bposlem2  20540  bposlem3  20541  bposlem4  20542  bposlem5  20543  bposlem6  20544  bposlem7  20545  bposlem9  20547  ipidsq  21302  ipasslem1  21425  ipasslem2  21426  ipasslem4  21428  ipasslem5  21429  ipasslem8  21431  ipasslem9  21432  ipasslem11  21434  pjoc1i  22026  h1de2bi  22149  h1de2ctlem  22150  spanunsni  22174  opsqrlem1  22736  opsqrlem6  22741  chrelati  22960  chrelat2i  22961  cvexchlem  22964  zetacvg  23704  erdszelem5  23741  fznatpl1  24108  axlowdim  24661  bpoly2  24864  bpoly3  24865  fsumcube  24867  nZdef  25283  expus  25468  heiborlem6  26643  onetansqsecsq  28485  cotsqcscsq  28486
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936
  Copyright terms: Public domain W3C validator