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

Theorem mp3an13 1364
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 1362 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 681 1  |-  ( ps 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 991
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 190  df-an 377  df-3an 993
This theorem is referenced by:  predeq2  5401  wrecseq2  7057  oeoalem  7322  mulid1  9665  addltmul  10876  eluzaddi  11213  fz01en  11855  fznatpl1  11878  expubnd  12364  bernneq  12429  bernneq2  12430  faclbnd4lem1  12509  hashfun  12641  bpoly2  14158  bpoly3  14159  fsumcube  14161  efi4p  14239  efival  14254  cos2tsin  14281  cos01bnd  14288  cos01gt0  14293  dvds0  14366  odd2np1  14413  divalglem0  14419  gcdid  14543  opoe  14809  pythagtriplem4  14817  ressid  15232  zringcyg  19108  lecldbas  20283  blssioo  21861  tgioo  21862  rerest  21870  xrrest  21873  zdis  21882  reconnlem2  21893  metdscn2  21922  metdscn2OLD  21937  negcncf  21998  iihalf2  22009  cncmet  22338  rrxmvallem  22406  rrxmval  22407  ovolunlem1a  22497  ismbf3d  22658  c1lip2  22998  pilem2  23455  pilem2OLD  23456  pilem3  23457  pilem3OLD  23458  sinperlem  23483  sincosq1sgn  23501  sincosq2sgn  23502  sinq12gt0  23510  cosq14gt0  23513  cosq14ge0  23514  coseq1  23525  sinord  23531  zetacvg  23988  1sgmprm  24175  ppiub  24180  chtublem  24187  chtub  24188  bcp1ctr  24255  bpos1lem  24258  bposlem2  24261  bposlem3  24262  bposlem4  24263  bposlem5  24264  bposlem6  24265  bposlem7  24266  bposlem9  24268  axlowdim  25039  2trllemD  25335  2trllemG  25336  constr1trl  25366  constr3lem4  25423  ipidsq  26397  ipasslem1  26520  ipasslem2  26521  ipasslem4  26523  ipasslem5  26524  ipasslem8  26526  ipasslem9  26527  ipasslem11  26529  pjoc1i  27132  h1de2bi  27255  h1de2ctlem  27256  spanunsni  27280  opsqrlem1  27841  opsqrlem6  27846  chrelati  28065  chrelat2i  28066  cvexchlem  28069  pnfinf  28548  rrhre  28873  erdszelem5  29966  wsuceq2  30547  taupilem1  31766  finxpreclem2  31826  sin2h  31979  cos2h  31980  tan2h  31981  poimirlem27  32011  poimirlem30  32014  broucube  32018  mblfinlem1  32021  heiborlem6  32192  icccncfext  37802  dirkertrigeq  38000  zlmodzxzel  40408  dignn0flhalflem1  40698  onetansqsecsq  40753  cotsqcscsq  40754
  Copyright terms: Public domain W3C validator