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

Theorem mp3an13 1351
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 1349 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 674 1  |-  ( ps 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 982
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 188  df-an 372  df-3an 984
This theorem is referenced by:  predeq2  5345  wrecseq2  6987  oeoalem  7252  mulid1  9591  addltmul  10799  eluzaddi  11136  fz01en  11778  fznatpl1  11801  expubnd  12283  bernneq  12348  bernneq2  12349  faclbnd4lem1  12428  hashfun  12557  bpoly2  14053  bpoly3  14054  fsumcube  14056  efi4p  14134  efival  14149  cos2tsin  14176  cos01bnd  14183  cos01gt0  14188  dvds0  14261  odd2np1  14308  divalglem0  14314  gcdid  14438  opoe  14704  pythagtriplem4  14712  ressid  15127  zringcyg  19002  lecldbas  20177  blssioo  21755  tgioo  21756  rerest  21764  xrrest  21767  zdis  21776  reconnlem2  21787  metdscn2  21816  metdscn2OLD  21831  negcncf  21892  iihalf2  21903  cncmet  22232  rrxmvallem  22300  rrxmval  22301  ovolunlem1a  22391  ismbf3d  22552  c1lip2  22892  pilem2  23349  pilem2OLD  23350  pilem3  23351  pilem3OLD  23352  sinperlem  23377  sincosq1sgn  23395  sincosq2sgn  23396  sinq12gt0  23404  cosq14gt0  23407  cosq14ge0  23408  coseq1  23419  sinord  23425  zetacvg  23882  1sgmprm  24069  ppiub  24074  chtublem  24081  chtub  24082  bcp1ctr  24149  bpos1lem  24152  bposlem2  24155  bposlem3  24156  bposlem4  24157  bposlem5  24158  bposlem6  24159  bposlem7  24160  bposlem9  24162  axlowdim  24933  2trllemD  25229  2trllemG  25230  constr1trl  25260  constr3lem4  25317  ipidsq  26291  ipasslem1  26414  ipasslem2  26415  ipasslem4  26417  ipasslem5  26418  ipasslem8  26420  ipasslem9  26421  ipasslem11  26423  pjoc1i  27026  h1de2bi  27149  h1de2ctlem  27150  spanunsni  27174  opsqrlem1  27735  opsqrlem6  27740  chrelati  27959  chrelat2i  27960  cvexchlem  27963  pnfinf  28451  rrhre  28777  erdszelem5  29870  wsuceq2  30450  taupilem1  31629  finxpreclem2  31689  sin2h  31842  cos2h  31843  tan2h  31844  poimirlem27  31874  poimirlem30  31877  broucube  31881  mblfinlem1  31884  heiborlem6  32055  icccncfext  37648  dirkertrigeq  37846  zlmodzxzel  39739  dignn0flhalflem1  40029  onetansqsecsq  40084  cotsqcscsq  40085
  Copyright terms: Public domain W3C validator