Theorem mprg 2777

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 2773	. 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 1726   A.wral 2707

This theorem is referenced by:  reximia  2813  rmoimia  3136  iuneq2i  4113  iineq2i  4114  dfiun2  4127  dfiin2  4128  eusv4  4735  reuxfr2d  4749  dfiun3  5127  dfiin3  5128  cnviin  5412  relmptopab  6295  ixpint  7092  noinfep  7617  tctr  7682  r1elssi  7734  ackbij2  8128  hsmexlem5  8315  axcc2lem  8321  inar1  8655  sumeq2i  12498  sum2id  12507  prdsbasex  13679  fnmrc  13837  sscpwex  14020  gsumwspan  14796  0frgp  15416  psrbaglefi  16442  mvrf1  16494  mplmonmul  16532  frgpcyg  16859  elpt  17609  ptbasin2  17615  ptbasfi  17618  ptcld  17650  ptrescn  17676  xkoinjcn  17724  ptuncnv  17844  ptunhmeo  17845  itgfsum  19721  rolle  19879  dvlip  19882  dvivthlem1  19897  dvivth  19899  pserdv  20350  logtayl  20556  goeqi  23781  reuxfr3d  23981  sxbrsigalem0  24626  cvmsss2  24966  cvmliftphtlem  25009  prodeq2i  25250  prod2id  25259  dfon2lem1  25415  dfon2lem3  25417  dfon2lem7  25421  mblfinlem2  26256  voliunnfl  26262  sdclem2  26460  dmmzp  26804  lhe4.4ex1a  27537  2reurmo  27950  bnj852  29366  bnj1145  29436

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

This theorem depends on definitions:  df-bi 179  df-ral 2712