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

Theorem mp3an13 1315
Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)
Hypotheses
Ref Expression
mp3an13.1
mp3an13.2
mp3an13.3
Assertion
Ref Expression
mp3an13

Proof of Theorem mp3an13
StepHypRef Expression
1 mp3an13.1 . 2
2 mp3an13.2 . . 3
3 mp3an13.3 . . 3
42, 3mp3an3 1313 . 2
51, 4mpan 670 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\w3a 973
This theorem is referenced by:  oeoalem  7264  mulid1  9614  addltmul  10799  uzindOLD  10982  eluzaddi  11136  fz01en  11742  fznatpl1  11763  expubnd  12226  bernneq  12292  bernneq2  12293  faclbnd4lem1  12371  hashfun  12495  efi4p  13872  efival  13887  cos2tsin  13914  cos01bnd  13921  cos01gt0  13926  dvds0  13999  odd2np1  14046  divalglem0  14051  gcdid  14169  opoe  14335  pythagtriplem4  14343  ressid  14692  zringcyg  18513  zcyg  18518  lecldbas  19720  blssioo  21300  tgioo  21301  rerest  21309  xrrest  21312  zdis  21321  reconnlem2  21332  metdscn2  21361  negcncf  21422  iihalf2  21433  cncmet  21761  rrxmvallem  21831  rrxmval  21832  ovolunlem1a  21907  ismbf3d  22061  c1lip2  22399  pilem2  22847  pilem3  22848  sinperlem  22873  sincosq1sgn  22891  sincosq2sgn  22892  sinq12gt0  22900  cosq14gt0  22903  cosq14ge0  22904  coseq1  22915  sinord  22921  1sgmprm  23474  ppiub  23479  chtublem  23486  chtub  23487  bcp1ctr  23554  bpos1lem  23557  bposlem2  23560  bposlem3  23561  bposlem4  23562  bposlem5  23563  bposlem6  23564  bposlem7  23565  bposlem9  23567  axlowdim  24264  2trllemD  24559  2trllemG  24560  constr1trl  24590  constr3lem4  24647  ipidsq  25623  ipasslem1  25746  ipasslem2  25747  ipasslem4  25749  ipasslem5  25750  ipasslem8  25752  ipasslem9  25753  ipasslem11  25755  pjoc1i  26349  h1de2bi  26472  h1de2ctlem  26473  spanunsni  26497  opsqrlem1  27059  opsqrlem6  27064  chrelati  27283  chrelat2i  27284  cvexchlem  27287  pnfinf  27727  rrhre  27999  zetacvg  28557  erdszelem5  28639  predeq2  29247  wrecseq2  29340  wsuceq2  29372  bpoly2  29819  bpoly3  29820  fsumcube  29822  sin2h  30045  cos2h  30046  tan2h  30047  mblfinlem1  30051  heiborlem6  30312  icccncfext  31690  dirkertrigeq  31883  zlmodzxzel  32944  onetansqsecsq  33155  cotsqcscsq  33156  taupilem1  37696
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 975
  Copyright terms: Public domain W3C validator