Theorem mprg 2612

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 2608	. 2 |- A. x e. A ph
3		mprg.1	. 2 |- ( A. x e. A ph -> ps )
4	2, 3	ax-mp 8	1 |- ps

Syntax hints:   -> wi 4   e. wcel 1684   A.wral 2543

This theorem is referenced by:  reximia  2648  rmoimia  2965  iuneq2i  3923  iineq2i  3924  dfiun2  3937  dfiin2  3938  eusv4  4543  reuxfr2d  4557  dfiun3  4933  dfiin3  4934  cnviin  5212  relmptopab  6065  ixpint  6843  noinfep  7360  tctr  7425  r1elssi  7477  ackbij2  7869  hsmexlem5  8056  axcc2lem  8062  inar1  8397  sumeq2i  12172  sum2id  12181  prdsbasex  13351  fnmrc  13509  sscpwex  13692  gsumwspan  14468  0frgp  15088  psrbaglefi  16118  mvrf1  16170  mplmonmul  16208  frgpcyg  16527  elpt  17267  ptbasin2  17273  ptbasfi  17276  ptcld  17307  ptrescn  17333  xkoinjcn  17381  ptuncnv  17498  ptunhmeo  17499  itgfsum  19181  rolle  19337  dvlip  19340  dvivthlem1  19355  dvivth  19357  pserdv  19805  logtayl  20007  goeqi  22853  reuxfr3d  23138  cvmsss2  23805  cvmliftphtlem  23848  dfon2lem1  24139  dfon2lem3  24141  dfon2lem7  24145  dstr  25171  svli2  25484  intopcoaconlem3  25539  smbkle  26043  pgapspf  26052  pgapspf2  26053  sdclem2  26452  dmmzp  26811  lhe4.4ex1a  27546  2reurmo  27960  bnj852  28953  bnj1145  29023

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

This theorem depends on definitions:  df-bi 177  df-ral 2548