Theorem mprg 2820

Description: Modus ponens combined with restricted generalization. (Contributed by NM, 10-Aug-2004.)

Hypotheses

Ref	Expression
mprg.1
mprg.2

Assertion

Ref	Expression
mprg

Proof of Theorem mprg

Step	Hyp	Ref	Expression
1		mprg.2	. . 3
2	1	rgen 2817	. 2
3		mprg.1	. 2
4	2, 3	ax-mp 5	1

Syntax hints:  ->wi 4  e.wcel 1818  A.wral 2807

This theorem is referenced by:  reximia  2923  rmoimia  3300  iuneq2i  4349  iineq2i  4350  dfiun2  4364  dfiin2  4365  eusv4  4661  reuxfr2d  4675  dfiun3  5262  dfiin3  5263  cnviin  5549  relmptopab  6523  ixpint  7516  noinfep  8097  tctr  8192  r1elssi  8244  ackbij2  8644  hsmexlem5  8831  axcc2lem  8837  inar1  9174  sumeq2i  13521  sum2id  13530  prodeq2i  13726  prod2id  13735  prdsbasex  14848  fnmrc  15004  sscpwex  15184  gsumwspan  16014  0frgp  16797  psrbaglefi  18023  psrbaglefiOLD  18024  mvrf1  18081  mplmonmul  18126  frgpcyg  18612  elpt  20073  ptbasin2  20079  ptbasfi  20082  ptcld  20114  ptrescn  20140  xkoinjcn  20188  ptuncnv  20308  ptunhmeo  20309  itgfsum  22233  rolle  22391  dvlip  22394  dvivthlem1  22409  dvivth  22411  pserdv  22824  logtayl  23041  goeqi  27192  reuxfr3d  27388  sxbrsigalem0  28242  cvmsss2  28719  cvmliftphtlem  28762  dfon2lem1  29215  dfon2lem3  29217  dfon2lem7  29221  ptrest  30048  mblfinlem2  30052  voliunnfl  30058  sdclem2  30235  dmmzp  30665  arearect  31183  areaquad  31184  lhe4.4ex1a  31234  dvcosax  31723  fourierdlem57  31946  fourierdlem58  31947  fourierdlem62  31951  2reurmo  32187  nnsgrpnmnd  32506  bnj852  33979  bnj1145  34049

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

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