Theorem mprg 2751

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 2747	. 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 1887   A.wral 2737

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

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

This theorem is referenced by:  reximia  2853  rmoimia  3240  iuneq2i  4297  iineq2i  4298  dfiun2  4312  dfiin2  4313  eusv4  4612  reuxfr2d  4623  dfiun3  5089  dfiin3  5090  cnviin  5373  relmptopab  6517  ixpint  7549  noinfep  8165  tctr  8224  r1elssi  8276  ackbij2  8673  hsmexlem5  8860  axcc2lem  8866  inar1  9200  sumeq2i  13765  sum2id  13774  prodeq2i  13973  prod2id  13982  prdsbasex  15349  fnmrc  15513  sscpwex  15720  gsumwspan  16630  0frgp  17429  psrbaglefi  18596  mvrf1  18649  mplmonmul  18688  frgpcyg  19144  elpt  20587  ptbasin2  20593  ptbasfi  20596  ptcld  20628  ptrescn  20654  xkoinjcn  20702  ptuncnv  20822  ptunhmeo  20823  itgfsum  22784  rolle  22942  dvlip  22945  dvivthlem1  22960  dvivth  22962  pserdv  23384  logtayl  23605  goeqi  27926  reuxfr3d  28125  sxbrsigalem0  29093  bnj852  29732  bnj1145  29802  cvmsss2  29997  cvmliftphtlem  30040  dfon2lem1  30429  dfon2lem3  30431  dfon2lem7  30435  ptrest  31939  mblfinlem2  31978  voliunnfl  31984  sdclem2  32071  dmmzp  35575  arearect  36100  areaquad  36101  trclrelexplem  36303  corcltrcl  36331  cotrclrcl  36334  lhe4.4ex1a  36678  dvcosax  37798  fourierdlem57  38027  fourierdlem58  38028  fourierdlem62  38032  2reurmo  38603  nnsgrpnmnd  39871  elbigofrcl  40414