Theorem mprg 2806

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 2803	. 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 1804   A.wral 2793

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

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

This theorem is referenced by:  reximia  2909  rmoimia  3286  iuneq2i  4334  iineq2i  4335  dfiun2  4349  dfiin2  4350  eusv4  4646  reuxfr2d  4660  dfiun3  5247  dfiin3  5248  cnviin  5534  relmptopab  6508  ixpint  7498  noinfep  8079  tctr  8174  r1elssi  8226  ackbij2  8626  hsmexlem5  8813  axcc2lem  8819  inar1  9156  sumeq2i  13503  sum2id  13512  prodeq2i  13708  prod2id  13717  prdsbasex  14830  fnmrc  14986  sscpwex  15166  gsumwspan  15993  0frgp  16776  psrbaglefi  18002  psrbaglefiOLD  18003  mvrf1  18060  mplmonmul  18105  frgpcyg  18590  elpt  20051  ptbasin2  20057  ptbasfi  20060  ptcld  20092  ptrescn  20118  xkoinjcn  20166  ptuncnv  20286  ptunhmeo  20287  itgfsum  22211  rolle  22369  dvlip  22372  dvivthlem1  22387  dvivth  22389  pserdv  22802  logtayl  23019  goeqi  27170  reuxfr3d  27366  sxbrsigalem0  28220  cvmsss2  28697  cvmliftphtlem  28740  dfon2lem1  29191  dfon2lem3  29193  dfon2lem7  29197  ptrest  30024  mblfinlem2  30028  voliunnfl  30034  sdclem2  30211  dmmzp  30641  arearect  31159  areaquad  31160  lhe4.4ex1a  31210  dvcosax  31677  fourierdlem57  31900  fourierdlem58  31901  fourierdlem62  31905  2reurmo  32141  nnsgrpnmnd  32459  bnj852  33847  bnj1145  33917