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

Theorem mp3an13 1298
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 1296 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 663 1  |-  ( ps 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 958
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 960
This theorem is referenced by:  oeoalem  7023  mulid1  9370  addltmul  10547  uzindOLD  10723  eluzaddi  10874  fz01en  11463  fznatpl1  11494  expubnd  11907  bernneq  11973  bernneq2  11974  faclbnd4lem1  12052  hashfun  12182  efi4p  13403  efival  13418  cos2tsin  13445  cos01bnd  13452  cos01gt0  13457  dvds0  13530  odd2np1  13574  divalglem0  13579  gcdid  13697  opoe  13860  pythagtriplem4  13868  ressid  14215  zringcyg  17748  zcyg  17753  lecldbas  18664  blssioo  20213  tgioo  20214  rerest  20222  xrrest  20225  zdis  20234  reconnlem2  20245  metdscn2  20274  negcncf  20335  iihalf2  20346  cncmet  20674  rrxmvallem  20744  rrxmval  20745  ovolunlem1a  20820  ismbf3d  20973  c1lip2  21311  pilem2  21801  pilem3  21802  sinperlem  21826  sincosq1sgn  21844  sincosq2sgn  21845  sinq12gt0  21853  cosq14gt0  21856  cosq14ge0  21857  coseq1  21868  sinord  21874  1sgmprm  22422  ppiub  22427  chtublem  22434  chtub  22435  bcp1ctr  22502  bpos1lem  22505  bposlem2  22508  bposlem3  22509  bposlem4  22510  bposlem5  22511  bposlem6  22512  bposlem7  22513  bposlem9  22515  axlowdim  23029  2trllemD  23278  2trllemG  23279  constr1trl  23309  constr3lem4  23355  ipidsq  23930  ipasslem1  24053  ipasslem2  24054  ipasslem4  24056  ipasslem5  24057  ipasslem8  24059  ipasslem9  24060  ipasslem11  24062  pjoc1i  24656  h1de2bi  24779  h1de2ctlem  24780  spanunsni  24804  opsqrlem1  25366  opsqrlem6  25371  chrelati  25590  chrelat2i  25591  cvexchlem  25594  pnfinf  26023  rrhre  26300  zetacvg  26848  erdszelem5  26930  predeq2  27474  wrecseq2  27567  wsuceq2  27599  bpoly2  28046  bpoly3  28047  fsumcube  28049  sin2h  28263  cos2h  28264  tan2h  28265  mblfinlem1  28269  heiborlem6  28556  zlmodzxzel  30583  onetansqsecsq  30802  cotsqcscsq  30803  taupilem1  35185
  Copyright terms: Public domain W3C validator