Theorem mprg 3062

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

Syntax hints:   → wi 4   ∈ wcel 2099  ∀wral 3056

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

This theorem depends on definitions:  df-bi 206  df-ral 3057

This theorem is referenced by:  reximiaOLD  3083  rmoimia  3734  reuxfrd  3741  2reurmo  3752  ralf0  4509  iuneq2i  5012  iineq2i  5013  dfiun2  5030  dfiin2  5031  eusv4  5400  dfiun3  5963  dfiin3  5964  relmptopab  7665  fsplitfpar  8117  ixpint  8935  noinfep  9675  tctr  9755  r1elssi  9820  ackbij2  10258  hsmexlem5  10445  axcc2lem  10451  inar1  10790  ccatalpha  14567  sumeq2i  15669  sum2id  15678  prodeq2i  15887  prod2id  15896  prdsbasex  17423  fnmrc  17578  sscpwex  17789  gsumwspan  18789  0frgp  19725  subdrgint  20680  frgpcyg  21494  psrbaglefi  21852  psrbaglefiOLD  21853  mvrf1  21915  mplmonmul  21961  elpt  23463  ptbasin2  23469  ptbasfi  23472  ptcld  23504  ptrescn  23530  xkoinjcn  23578  ptuncnv  23698  ptunhmeo  23699  itgfsum  25743  rolle  25909  dvlip  25913  dvivthlem1  25928  dvivth  25930  pserdv  26353  logtayl  26581  goeqi  32070  reuxfrdf  32275  sxbrsigalem0  33827  bnj852  34488  bnj1145  34560  cvmsss2  34820  cvmliftphtlem  34863  dfon2lem1  35315  dfon2lem3  35317  dfon2lem7  35321  ptrest  37027  mblfinlem2  37066  voliunnfl  37072  sdclem2  37150  dmmzp  42075  arearect  42566  areaquad  42567  trclrelexplem  43064  corcltrcl  43092  cotrclrcl  43095  clsk3nimkb  43393  lhe4.4ex1a  43689  dvcosax  45237  fourierdlem57  45474  fourierdlem58  45475  fourierdlem62  45479  nnsgrpnmnd  47163  elbigofrcl  47546  iunordi  48031