Theorem mprg 2743

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 2739	. 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 1721   A.wral 2674

This theorem is referenced by:  reximia  2779  rmoimia  3102  iuneq2i  4079  iineq2i  4080  dfiun2  4093  dfiin2  4094  eusv4  4699  reuxfr2d  4713  dfiun3  5091  dfiin3  5092  cnviin  5376  relmptopab  6259  ixpint  7056  noinfep  7578  tctr  7643  r1elssi  7695  ackbij2  8087  hsmexlem5  8274  axcc2lem  8280  inar1  8614  sumeq2i  12456  sum2id  12465  prdsbasex  13637  fnmrc  13795  sscpwex  13978  gsumwspan  14754  0frgp  15374  psrbaglefi  16400  mvrf1  16452  mplmonmul  16490  frgpcyg  16817  elpt  17565  ptbasin2  17571  ptbasfi  17574  ptcld  17606  ptrescn  17632  xkoinjcn  17680  ptuncnv  17800  ptunhmeo  17801  itgfsum  19679  rolle  19835  dvlip  19838  dvivthlem1  19853  dvivth  19855  pserdv  20306  logtayl  20512  goeqi  23737  reuxfr3d  23937  sxbrsigalem0  24582  cvmsss2  24922  cvmliftphtlem  24965  prodeq2i  25206  prod2id  25215  dfon2lem1  25361  dfon2lem3  25363  dfon2lem7  25367  mblfinlem  26151  voliunnfl  26157  sdclem2  26344  dmmzp  26688  lhe4.4ex1a  27422  2reurmo  27835  bnj852  29010  bnj1145  29080

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

This theorem depends on definitions:  df-bi 178  df-ral 2679