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

Theorem mp3an13 1271
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 1269 . 2  |-  ( (
ph  /\  ps )  ->  th )
51, 4mpan 653 1  |-  ( ps 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 937
This theorem is referenced by:  oeoalem  6841  mulid1  9090  addltmul  10205  uzindOLD  10366  eluzaddi  10514  fz01en  11081  expubnd  11442  bernneq  11507  bernneq2  11508  faclbnd4lem1  11586  hashfun  11702  efi4p  12740  efival  12755  cos2tsin  12782  cos01bnd  12789  cos01gt0  12794  dvds0  12867  odd2np1  12910  divalglem0  12915  gcdid  13033  opoe  13187  pythagtriplem4  13195  ressid  13526  zcyg  16774  lecldbas  17285  blssioo  18828  tgioo  18829  rerest  18837  xrrest  18840  zdis  18849  reconnlem2  18860  metdscn2  18889  negcncf  18950  iihalf2  18960  cncmet  19277  ovolunlem1a  19394  ismbf3d  19548  c1lip2  19884  pilem2  20370  pilem3  20371  sinperlem  20390  sincosq1sgn  20408  sincosq2sgn  20409  sinq12gt0  20417  cosq14gt0  20420  cosq14ge0  20421  coseq1  20432  sinord  20438  1sgmprm  20985  ppiub  20990  chtublem  20997  chtub  20998  bcp1ctr  21065  bpos1lem  21068  bposlem2  21071  bposlem3  21072  bposlem4  21073  bposlem5  21074  bposlem6  21075  bposlem7  21076  bposlem9  21078  2trllemD  21559  2trllemG  21560  constr1trl  21590  constr3lem4  21636  ipidsq  22211  ipasslem1  22334  ipasslem2  22335  ipasslem4  22337  ipasslem5  22338  ipasslem8  22340  ipasslem9  22341  ipasslem11  22343  pjoc1i  22935  h1de2bi  23058  h1de2ctlem  23059  spanunsni  23083  opsqrlem1  23645  opsqrlem6  23650  chrelati  23869  chrelat2i  23870  cvexchlem  23873  pnfinf  24255  rrhre  24389  zetacvg  24801  erdszelem5  24883  fznatpl1  25200  predeq2  25444  wrecseq2  25537  wsuceq2  25569  axlowdim  25902  bpoly2  26105  bpoly3  26106  fsumcube  26108  mblfinlem1  26245  heiborlem6  26527  onetansqsecsq  28566  cotsqcscsq  28567
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939
  Copyright terms: Public domain W3C validator