Theorem mprg 3082

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  rmoimia  3698  reuxfrd  3705  2reurmo  3716  rabxm  4339  iuneq2i  4972  iineq2i  4973  dfiun2  4989  dfiin2  4990  eusv4  5367  dfiun3  5951  dfiin3  5952  relmptopab  7671  fsplitfpar  8129  ixpint  8953  noinfep  9661  tctr  9739  r1elssi  9813  ackbij2  10320  hsmexlem5  10508  axcc2lem  10514  inar1  10860  ccatalpha  14740  sgnrn  15251  sumeq2i  15865  sum2id  15874  prodeq2i  16086  prod2id  16095  prdsbasex  17621  fnmrc  17781  sscpwex  17990  gsumwspan  19042  0frgp  19993  subdrgint  21060  frgpcyg  21879  psrbaglefi  22234  mvrf1  22293  mplmonmul  22345  elpt  23891  ptbasin2  23897  ptbasfi  23900  ptcld  23932  ptrescn  23958  xkoinjcn  24006  ptuncnv  24126  ptunhmeo  24127  itgfsum  26147  rolle  26310  dvlip  26313  dvivthlem1  26328  dvivth  26330  pserdv  26756  logtayl  26988  goeqi  32875  reuxfrdf  33129  psrmonmul  34224  sxbrsigalem0  34945  bnj852  35593  bnj1145  35665  tz9.1regs  35844  cvmsss2  36081  cvmliftphtlem  36124  dfon2lem1  36587  dfon2lem3  36589  dfon2lem7  36593  disjeq12i  37024  ptrest  38580  mblfinlem2  38619  voliunnfl  38625  sdclem2  38719  dmmzp  43787  arearect  44260  areaquad  44261  trclrelexplem  44754  corcltrcl  44782  cotrclrcl  44785  clsk3nimkb  45083  lhe4.4ex1a  45356  wfaxsep  46028  wfaxpow  46030  wfaxun  46032  dvcosax  46979  fourierdlem57  47216  fourierdlem58  47217  fourierdlem62  47221  nnsgrpnmnd  49318  elbigofrcl  49705  iunordi  50828