Theorem mprg 3077

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3063

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

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

This theorem is referenced by:  reximiaOLD  3173  rmoimia  3671  reuxfrd  3678  2reurmo  3689  ralf0  4441  iuneq2i  4942  iineq2i  4943  dfiun2  4959  dfiin2  4960  eusv4  5324  dfiun3  5864  dfiin3  5865  relmptopab  7497  fsplitfpar  7930  ixpint  8671  noinfep  9348  tctr  9429  r1elssi  9494  ackbij2  9930  hsmexlem5  10117  axcc2lem  10123  inar1  10462  ccatalpha  14226  sumeq2i  15339  sum2id  15348  prodeq2i  15557  prod2id  15566  prdsbasex  17078  fnmrc  17233  sscpwex  17444  gsumwspan  18400  0frgp  19300  subdrgint  19986  frgpcyg  20693  psrbaglefi  21045  psrbaglefiOLD  21046  mvrf1  21104  mplmonmul  21147  elpt  22631  ptbasin2  22637  ptbasfi  22640  ptcld  22672  ptrescn  22698  xkoinjcn  22746  ptuncnv  22866  ptunhmeo  22867  itgfsum  24896  rolle  25059  dvlip  25062  dvivthlem1  25077  dvivth  25079  pserdv  25493  logtayl  25720  goeqi  30536  reuxfrdf  30740  sxbrsigalem0  32138  bnj852  32801  bnj1145  32873  cvmsss2  33136  cvmliftphtlem  33179  dfon2lem1  33665  dfon2lem3  33667  dfon2lem7  33671  ptrest  35703  mblfinlem2  35742  voliunnfl  35748  sdclem2  35827  dmmzp  40471  arearect  40962  areaquad  40963  trclrelexplem  41208  corcltrcl  41236  cotrclrcl  41239  clsk3nimkb  41539  lhe4.4ex1a  41836  dvcosax  43357  fourierdlem57  43594  fourierdlem58  43595  fourierdlem62  43599  nnsgrpnmnd  45260  elbigofrcl  45784  iunordi  46269