Theorem mprg 3056

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3050

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

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

This theorem is referenced by:  rmoimia  3729  reuxfrd  3736  2reurmo  3747  rabxm  4370  ralf0  4494  iuneq2i  4993  iineq2i  4994  dfiun2  5013  dfiin2  5014  eusv4  5386  dfiun3  5960  dfiin3  5961  relmptopab  7665  fsplitfpar  8125  ixpint  8947  noinfep  9682  tctr  9762  r1elssi  9827  ackbij2  10264  hsmexlem5  10452  axcc2lem  10458  inar1  10797  ccatalpha  14613  sumeq2i  15716  sum2id  15726  prodeq2i  15936  prod2id  15946  prdsbasex  17466  fnmrc  17621  sscpwex  17830  gsumwspan  18828  0frgp  19765  subdrgint  20772  frgpcyg  21546  psrbaglefi  21900  mvrf1  21960  mplmonmul  22008  elpt  23526  ptbasin2  23532  ptbasfi  23535  ptcld  23567  ptrescn  23593  xkoinjcn  23641  ptuncnv  23761  ptunhmeo  23762  itgfsum  25798  rolle  25964  dvlip  25968  dvivthlem1  25983  dvivth  25985  pserdv  26409  logtayl  26638  goeqi  32220  reuxfrdf  32438  sxbrsigalem0  34232  bnj852  34894  bnj1145  34966  cvmsss2  35238  cvmliftphtlem  35281  dfon2lem1  35743  dfon2lem3  35745  dfon2lem7  35749  disjeq12i  36153  ptrest  37585  mblfinlem2  37624  voliunnfl  37630  sdclem2  37708  dmmzp  42707  arearect  43190  areaquad  43191  trclrelexplem  43686  corcltrcl  43714  cotrclrcl  43717  clsk3nimkb  44015  lhe4.4ex1a  44305  wfaxsep  44969  wfaxpow  44971  wfaxun  44973  dvcosax  45898  fourierdlem57  46135  fourierdlem58  46136  fourierdlem62  46140  nnsgrpnmnd  48052  elbigofrcl  48429  iunordi  49204