Theorem mprg 2770

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 2766	. 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 1904   A.wral 2756

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

This theorem depends on definitions:  df-bi 190  df-ral 2761

This theorem is referenced by:  reximia  2850  rmoimia  3228  iuneq2i  4288  iineq2i  4289  dfiun2  4303  dfiin2  4304  eusv4  4610  reuxfr2d  4623  dfiun3  5095  dfiin3  5096  cnviin  5380  relmptopab  6536  ixpint  7567  noinfep  8183  tctr  8242  r1elssi  8294  ackbij2  8691  hsmexlem5  8878  axcc2lem  8884  inar1  9218  ccatalpha  12787  sumeq2i  13842  sum2id  13851  prodeq2i  14050  prod2id  14059  prdsbasex  15427  fnmrc  15591  sscpwex  15798  gsumwspan  16708  0frgp  17507  psrbaglefi  18673  mvrf1  18726  mplmonmul  18765  frgpcyg  19221  elpt  20664  ptbasin2  20670  ptbasfi  20673  ptcld  20705  ptrescn  20731  xkoinjcn  20779  ptuncnv  20899  ptunhmeo  20900  itgfsum  22863  rolle  23021  dvlip  23024  dvivthlem1  23039  dvivth  23041  pserdv  23463  logtayl  23684  goeqi  28007  reuxfr3d  28204  sxbrsigalem0  29166  bnj852  29804  bnj1145  29874  cvmsss2  30069  cvmliftphtlem  30112  dfon2lem1  30500  dfon2lem3  30502  dfon2lem7  30506  ptrest  32003  mblfinlem2  32042  voliunnfl  32048  sdclem2  32135  dmmzp  35646  arearect  36171  areaquad  36172  trclrelexplem  36374  corcltrcl  36402  cotrclrcl  36405  lhe4.4ex1a  36748  dvcosax  37895  fourierdlem57  38139  fourierdlem58  38140  fourierdlem62  38144  2reurmo  38748  nnsgrpnmnd  40326  elbigofrcl  40869