Theorem mprg 3050

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 3046	. 2 ⊢ ∀𝑥 ∈ 𝐴 𝜑
3		mprg.1	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 → 𝜓)
4	2, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

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

This theorem depends on definitions:  df-bi 207  df-ral 3045

This theorem is referenced by:  rmoimia  3703  reuxfrd  3710  2reurmo  3721  rabxm  4343  ralf0  4467  iuneq2i  4966  iineq2i  4967  dfiun2  4985  dfiin2  4986  eusv4  5348  dfiun3  5915  dfiin3  5916  relmptopab  7603  fsplitfpar  8058  ixpint  8859  noinfep  9575  tctr  9655  r1elssi  9720  ackbij2  10155  hsmexlem5  10343  axcc2lem  10349  inar1  10688  ccatalpha  14518  sumeq2i  15623  sum2id  15633  prodeq2i  15843  prod2id  15853  prdsbasex  17372  fnmrc  17531  sscpwex  17740  gsumwspan  18738  0frgp  19676  subdrgint  20706  frgpcyg  21498  psrbaglefi  21851  mvrf1  21911  mplmonmul  21959  elpt  23475  ptbasin2  23481  ptbasfi  23484  ptcld  23516  ptrescn  23542  xkoinjcn  23590  ptuncnv  23710  ptunhmeo  23711  itgfsum  25744  rolle  25910  dvlip  25914  dvivthlem1  25929  dvivth  25931  pserdv  26355  logtayl  26585  goeqi  32235  reuxfrdf  32453  sxbrsigalem0  34238  bnj852  34887  bnj1145  34959  tz9.1regs  35066  cvmsss2  35246  cvmliftphtlem  35289  dfon2lem1  35756  dfon2lem3  35758  dfon2lem7  35762  disjeq12i  36166  ptrest  37598  mblfinlem2  37637  voliunnfl  37643  sdclem2  37721  dmmzp  42706  arearect  43188  areaquad  43189  trclrelexplem  43684  corcltrcl  43712  cotrclrcl  43715  clsk3nimkb  44013  lhe4.4ex1a  44302  wfaxsep  44969  wfaxpow  44971  wfaxun  44973  dvcosax  45908  fourierdlem57  46145  fourierdlem58  46146  fourierdlem62  46150  nnsgrpnmnd  48150  elbigofrcl  48523  iunordi  49650