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

Theorem mprg 2697
Description: Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)
Hypotheses
Ref Expression
mprg.1  |-  ( A. x  e.  A  ph  ->  ps )
mprg.2  |-  ( x  e.  A  ->  ph )
Assertion
Ref Expression
mprg  |-  ps

Proof of Theorem mprg
StepHypRef Expression
1 mprg.2 . . 3  |-  ( x  e.  A  ->  ph )
21rgen 2693 . 2  |-  A. x  e.  A  ph
3 mprg.1 . 2  |-  ( A. x  e.  A  ph  ->  ps )
42, 3ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1715   A.wral 2628
This theorem is referenced by:  reximia  2733  rmoimia  3051  iuneq2i  4025  iineq2i  4026  dfiun2  4039  dfiin2  4040  eusv4  4646  reuxfr2d  4660  dfiun3  5036  dfiin3  5037  cnviin  5315  relmptopab  6192  ixpint  6986  noinfep  7507  tctr  7572  r1elssi  7624  ackbij2  8016  hsmexlem5  8203  axcc2lem  8209  inar1  8544  sumeq2i  12380  sum2id  12389  prdsbasex  13561  fnmrc  13719  sscpwex  13902  gsumwspan  14678  0frgp  15298  psrbaglefi  16328  mvrf1  16380  mplmonmul  16418  frgpcyg  16744  elpt  17484  ptbasin2  17490  ptbasfi  17493  ptcld  17524  ptrescn  17550  xkoinjcn  17598  ptuncnv  17715  ptunhmeo  17716  itgfsum  19396  rolle  19552  dvlip  19555  dvivthlem1  19570  dvivth  19572  pserdv  20023  logtayl  20229  goeqi  23287  reuxfr3d  23491  cvmsss2  24529  cvmliftphtlem  24572  prodeq2i  24814  prod2id  24823  dfon2lem1  24965  dfon2lem3  24967  dfon2lem7  24971  voliunnfl  25758  sdclem2  26044  dmmzp  26402  lhe4.4ex1a  27137  2reurmo  27551  bnj852  28705  bnj1145  28775
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551
This theorem depends on definitions:  df-bi 177  df-ral 2633
  Copyright terms: Public domain W3C validator