Theorem mprg 2789

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 2786	. 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 1869   A.wral 2776

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

This theorem depends on definitions:  df-bi 189  df-ral 2781

This theorem is referenced by:  reximia  2892  rmoimia  3273  iuneq2i  4316  iineq2i  4317  dfiun2  4331  dfiin2  4332  eusv4  4631  reuxfr2d  4642  dfiun3  5106  dfiin3  5107  cnviin  5390  relmptopab  6529  ixpint  7555  noinfep  8168  tctr  8227  r1elssi  8279  ackbij2  8675  hsmexlem5  8862  axcc2lem  8868  inar1  9202  sumeq2i  13758  sum2id  13767  prodeq2i  13966  prod2id  13975  prdsbasex  15342  fnmrc  15506  sscpwex  15713  gsumwspan  16623  0frgp  17422  psrbaglefi  18589  mvrf1  18642  mplmonmul  18681  frgpcyg  19136  elpt  20579  ptbasin2  20585  ptbasfi  20588  ptcld  20620  ptrescn  20646  xkoinjcn  20694  ptuncnv  20814  ptunhmeo  20815  itgfsum  22776  rolle  22934  dvlip  22937  dvivthlem1  22952  dvivth  22954  pserdv  23376  logtayl  23597  goeqi  27918  reuxfr3d  28117  sxbrsigalem0  29095  bnj852  29734  bnj1145  29804  cvmsss2  29999  cvmliftphtlem  30042  dfon2lem1  30430  dfon2lem3  30432  dfon2lem7  30436  ptrest  31897  mblfinlem2  31936  voliunnfl  31942  sdclem2  32029  dmmzp  35538  arearect  36064  areaquad  36065  trclrelexplem  36207  corcltrcl  36235  cotrclrcl  36238  lhe4.4ex1a  36580  dvcosax  37662  fourierdlem57  37891  fourierdlem58  37892  fourierdlem62  37896  2reurmo  38360  nnsgrpnmnd  39160  elbigofrcl  39705