Theorem mprg 2827

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

Step	Hyp	Ref	Expression
1		mprg.2	. . 3 |- ( x e. A -> ph )
2	1	rgen 2824	. 2 |- A. x e. A ph
3		mprg.1	. 2 |- ( A. x e. A ph -> ps )
4	2, 3	ax-mp 5	1 |- ps

Syntax hints:   -> wi 4   e. wcel 1767   A.wral 2814

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601

This theorem depends on definitions:  df-bi 185  df-ral 2819

This theorem is referenced by:  reximia  2930  rmoimia  3304  iuneq2i  4344  iineq2i  4345  dfiun2  4359  dfiin2  4360  eusv4  4656  reuxfr2d  4670  dfiun3  5255  dfiin3  5256  cnviin  5542  relmptopab  6505  ixpint  7493  noinfep  8072  tctr  8167  r1elssi  8219  ackbij2  8619  hsmexlem5  8806  axcc2lem  8812  inar1  9149  sumeq2i  13480  sum2id  13489  prdsbasex  14702  fnmrc  14858  sscpwex  15041  gsumwspan  15837  0frgp  16593  psrbaglefi  17794  psrbaglefiOLD  17795  mvrf1  17852  mplmonmul  17897  frgpcyg  18379  elpt  19808  ptbasin2  19814  ptbasfi  19817  ptcld  19849  ptrescn  19875  xkoinjcn  19923  ptuncnv  20043  ptunhmeo  20044  itgfsum  21968  rolle  22126  dvlip  22129  dvivthlem1  22144  dvivth  22146  pserdv  22558  logtayl  22769  goeqi  26868  reuxfr3d  27064  sxbrsigalem0  27882  cvmsss2  28359  cvmliftphtlem  28402  prodeq2i  28628  prod2id  28637  dfon2lem1  28792  dfon2lem3  28794  dfon2lem7  28798  ptrest  29625  mblfinlem2  29629  voliunnfl  29635  sdclem2  29838  dmmzp  30269  arearect  30788  areaquad  30789  lhe4.4ex1a  30834  2reurmo  31654  bnj852  33058  bnj1145  33128