Theorem mprg 2871

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 2867	. 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 1757   A.wral 2792

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

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

This theorem is referenced by:  reximia  2903  rmoimia  3243  iuneq2i  4273  iineq2i  4274  dfiun2  4288  dfiin2  4289  eusv4  4585  reuxfr2d  4599  dfiun3  5178  dfiin3  5179  cnviin  5458  relmptopab  6394  ixpint  7376  noinfep  7952  tctr  8047  r1elssi  8099  ackbij2  8499  hsmexlem5  8686  axcc2lem  8692  inar1  9029  sumeq2i  13264  sum2id  13273  prdsbasex  14477  fnmrc  14633  sscpwex  14816  gsumwspan  15612  0frgp  16366  psrbaglefi  17533  psrbaglefiOLD  17534  mvrf1  17591  mplmonmul  17636  frgpcyg  18101  elpt  19247  ptbasin2  19253  ptbasfi  19256  ptcld  19288  ptrescn  19314  xkoinjcn  19362  ptuncnv  19482  ptunhmeo  19483  itgfsum  21406  rolle  21564  dvlip  21567  dvivthlem1  21582  dvivth  21584  pserdv  21996  logtayl  22207  goeqi  25798  reuxfr3d  25994  sxbrsigalem0  26806  cvmsss2  27283  cvmliftphtlem  27326  prodeq2i  27552  prod2id  27561  dfon2lem1  27716  dfon2lem3  27718  dfon2lem7  27722  ptrest  28549  mblfinlem2  28553  voliunnfl  28559  sdclem2  28762  dmmzp  29193  arearect  29715  areaquad  29716  lhe4.4ex1a  29727  2reurmo  30130  bnj852  32196  bnj1145  32266