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

Theorem mp3an13 1315
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 1313 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 670 1  |-  ( ps 
->  th )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ w3a 973
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
This theorem is referenced by:  oeoalem  7242  mulid1  9589  addltmul  10770  uzindOLD  10951  eluzaddi  11104  fz01en  11709  fznatpl1  11730  expubnd  12190  bernneq  12256  bernneq2  12257  faclbnd4lem1  12335  hashfun  12457  efi4p  13729  efival  13744  cos2tsin  13771  cos01bnd  13778  cos01gt0  13783  dvds0  13856  odd2np1  13901  divalglem0  13906  gcdid  14024  opoe  14190  pythagtriplem4  14198  ressid  14546  zringcyg  18280  zcyg  18285  lecldbas  19486  blssioo  21035  tgioo  21036  rerest  21044  xrrest  21047  zdis  21056  reconnlem2  21067  metdscn2  21096  negcncf  21157  iihalf2  21168  cncmet  21496  rrxmvallem  21566  rrxmval  21567  ovolunlem1a  21642  ismbf3d  21796  c1lip2  22134  pilem2  22581  pilem3  22582  sinperlem  22606  sincosq1sgn  22624  sincosq2sgn  22625  sinq12gt0  22633  cosq14gt0  22636  cosq14ge0  22637  coseq1  22648  sinord  22654  1sgmprm  23202  ppiub  23207  chtublem  23214  chtub  23215  bcp1ctr  23282  bpos1lem  23285  bposlem2  23288  bposlem3  23289  bposlem4  23290  bposlem5  23291  bposlem6  23292  bposlem7  23293  bposlem9  23295  axlowdim  23940  2trllemD  24235  2trllemG  24236  constr1trl  24266  constr3lem4  24323  ipidsq  25299  ipasslem1  25422  ipasslem2  25423  ipasslem4  25425  ipasslem5  25426  ipasslem8  25428  ipasslem9  25429  ipasslem11  25431  pjoc1i  26025  h1de2bi  26148  h1de2ctlem  26149  spanunsni  26173  opsqrlem1  26735  opsqrlem6  26740  chrelati  26959  chrelat2i  26960  cvexchlem  26963  pnfinf  27389  rrhre  27635  zetacvg  28197  erdszelem5  28279  predeq2  28824  wrecseq2  28917  wsuceq2  28949  bpoly2  29396  bpoly3  29397  fsumcube  29399  sin2h  29622  cos2h  29623  tan2h  29624  mblfinlem1  29628  heiborlem6  29915  zlmodzxzel  32008  onetansqsecsq  32236  cotsqcscsq  32237  taupilem1  36767
  Copyright terms: Public domain W3C validator