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

Theorem mprg 2755
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 2752 . 2  |-  A. x  e.  A  ph
3 mprg.1 . 2  |-  ( A. x  e.  A  ph  ->  ps )
42, 3ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1836   A.wral 2742
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1633
This theorem depends on definitions:  df-bi 185  df-ral 2747
This theorem is referenced by:  reximia  2858  rmoimia  3238  iuneq2i  4275  iineq2i  4276  dfiun2  4290  dfiin2  4291  eusv4  4587  reuxfr2d  4598  dfiun3  5183  dfiin3  5184  cnviin  5466  relmptopab  6440  ixpint  7433  noinfep  8008  tctr  8102  r1elssi  8154  ackbij2  8554  hsmexlem5  8741  axcc2lem  8747  inar1  9082  sumeq2i  13542  sum2id  13551  prodeq2i  13747  prod2id  13756  prdsbasex  14877  fnmrc  15033  sscpwex  15240  gsumwspan  16150  0frgp  16933  psrbaglefi  18155  psrbaglefiOLD  18156  mvrf1  18213  mplmonmul  18258  frgpcyg  18722  elpt  20177  ptbasin2  20183  ptbasfi  20186  ptcld  20218  ptrescn  20244  xkoinjcn  20292  ptuncnv  20412  ptunhmeo  20413  itgfsum  22337  rolle  22495  dvlip  22498  dvivthlem1  22513  dvivth  22515  pserdv  22928  logtayl  23147  goeqi  27329  reuxfr3d  27528  sxbrsigalem0  28434  cvmsss2  28944  cvmliftphtlem  28987  dfon2lem1  29416  dfon2lem3  29418  dfon2lem7  29422  ptrest  30249  mblfinlem2  30253  voliunnfl  30259  sdclem2  30437  dmmzp  30867  arearect  31387  areaquad  31388  lhe4.4ex1a  31438  dvcosax  31924  fourierdlem57  32147  fourierdlem58  32148  fourierdlem62  32152  2reurmo  32388  nnsgrpnmnd  32859  elbigofrcl  33406  bnj852  34361  bnj1145  34431  trclrelexplem  38282  corcltrcl  38284  cotrclrcl  38285
  Copyright terms: Public domain W3C validator