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  6594  mulid1  8835  addltmul  9947  uzindOLD  10106  eluzaddi  10254  fz01en  10818  expubnd  11162  bernneq  11227  bernneq2  11228  faclbnd4lem1  11306  hashfun  11389  efi4p  12417  efival  12432  cos2tsin  12459  cos01bnd  12466  cos01gt0  12471  dvds0  12544  odd2np1  12587  divalglem0  12592  gcdid  12710  opoe  12864  pythagtriplem4  12872  ressid  13203  zcyg  16445  lecldbas  16949  blssioo  18301  tgioo  18302  rerest  18310  xrrest  18313  zdis  18322  reconnlem2  18332  metdscn2  18361  negcncf  18421  iihalf2  18431  cncmet  18744  ovolunlem1a  18855  ismbf3d  19009  c1lip2  19345  pilem2  19828  pilem3  19829  sinperlem  19848  sincosq1sgn  19866  sincosq2sgn  19867  sinq12gt0  19875  cosq14gt0  19878  cosq14ge0  19879  coseq1  19890  sinord  19896  1sgmprm  20438  ppiub  20443  chtublem  20450  chtub  20451  bcp1ctr  20518  bpos1lem  20521  bposlem2  20524  bposlem3  20525  bposlem4  20526  bposlem5  20527  bposlem6  20528  bposlem7  20529  bposlem9  20531  ipidsq  21286  ipasslem1  21409  ipasslem2  21410  ipasslem4  21412  ipasslem5  21413  ipasslem8  21415  ipasslem9  21416  ipasslem11  21418  pjoc1i  22010  h1de2bi  22133  h1de2ctlem  22134  spanunsni  22158  opsqrlem1  22720  opsqrlem6  22725  chrelati  22944  chrelat2i  22945  cvexchlem  22948  zetacvg  23689  erdszelem5  23726  fznatpl1  24093  axlowdim  24589  bpoly2  24792  bpoly3  24793  fsumcube  24795  nZdef  25180  expus  25365  heiborlem6  26540  onetansqsecsq  28231  cotsqcscsq  28232
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