Theorem mprg 2926

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 2922	. 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 1990   A.wral 2912

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

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  reximia  3009  rmoimia  3408  iuneq2i  4539  iineq2i  4540  dfiun2  4554  dfiin2  4555  eusv4  4877  reuxfr2d  4891  dfiun3  5380  dfiin3  5381  relmptopab  6883  ixpint  7935  noinfep  8557  tctr  8616  r1elssi  8668  ackbij2  9065  hsmexlem5  9252  axcc2lem  9258  inar1  9597  ccatalpha  13375  sumeq2i  14429  sum2id  14439  prodeq2i  14649  prod2id  14658  prdsbasex  16111  fnmrc  16267  sscpwex  16475  gsumwspan  17383  0frgp  18192  psrbaglefi  19372  mvrf1  19425  mplmonmul  19464  frgpcyg  19922  elpt  21375  ptbasin2  21381  ptbasfi  21384  ptcld  21416  ptrescn  21442  xkoinjcn  21490  ptuncnv  21610  ptunhmeo  21611  itgfsum  23593  rolle  23753  dvlip  23756  dvivthlem1  23771  dvivth  23773  pserdv  24183  logtayl  24406  goeqi  29132  reuxfr3d  29329  sxbrsigalem0  30333  bnj852  30991  bnj1145  31061  cvmsss2  31256  cvmliftphtlem  31299  dfon2lem1  31688  dfon2lem3  31690  dfon2lem7  31694  ptrest  33408  mblfinlem2  33447  voliunnfl  33453  sdclem2  33538  dmmzp  37296  arearect  37801  areaquad  37802  trclrelexplem  38003  corcltrcl  38031  cotrclrcl  38034  clsk3nimkb  38338  lhe4.4ex1a  38528  dvcosax  40141  fourierdlem57  40380  fourierdlem58  40381  fourierdlem62  40385  2reurmo  41182  nnsgrpnmnd  41818  elbigofrcl  42344  iunordi  42423