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 2145  ∀wral 3076

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

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  5948  dfiin3  5949  relmptopab  7659  fsplitfpar  8112  ixpint  8931  noinfep  9639  tctr  9717  r1elssi  9787  ackbij2  10291  hsmexlem5  10479  axcc2lem  10485  inar1  10831  ccatalpha  14707  sgnrn  15218  sumeq2i  15832  sum2id  15841  prodeq2i  16053  prod2id  16062  prdsbasex  17582  fnmrc  17742  sscpwex  17951  gsumwspan  19003  0frgp  19954  subdrgint  21021  frgpcyg  21840  psrbaglefi  22195  mvrf1  22254  mplmonmul  22306  elpt  23852  ptbasin2  23858  ptbasfi  23861  ptcld  23893  ptrescn  23919  xkoinjcn  23967  ptuncnv  24087  ptunhmeo  24088  itgfsum  26108  rolle  26271  dvlip  26274  dvivthlem1  26289  dvivth  26291  pserdv  26719  logtayl  26951  goeqi  32808  reuxfrdf  33020  psrmonmul  34115  sxbrsigalem0  34837  bnj852  35485  bnj1145  35557  tz9.1regs  35727  cvmsss2  35960  cvmliftphtlem  36003  dfon2lem1  36467  dfon2lem3  36469  dfon2lem7  36473  disjeq12i  36904  ptrest  38457  mblfinlem2  38496  voliunnfl  38502  sdclem2  38596  dmmzp  43682  arearect  44160  areaquad  44161  trclrelexplem  44655  corcltrcl  44683  cotrclrcl  44686  clsk3nimkb  44984  lhe4.4ex1a  45257  wfaxsep  45922  wfaxpow  45924  wfaxun  45926  dvcosax  46858  fourierdlem57  47095  fourierdlem58  47096  fourierdlem62  47100  nnsgrpnmnd  49197  elbigofrcl  49584  iunordi  50707