Theorem mprg 3083

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3077

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 3078

This theorem is used by:  rmoimia  3699  reuxfrd  3706  2reurmo  3717  rabxm  4340  iuneq2i  4973  iineq2i  4974  dfiun2  4990  dfiin2  4991  eusv4  5368  dfiun3  5952  dfiin3  5953  relmptopab  7672  fsplitfpar  8130  ixpint  8954  noinfep  9662  tctr  9740  r1elssi  9814  ackbij2  10321  hsmexlem5  10509  axcc2lem  10515  inar1  10861  ccatalpha  14741  sgnrn  15252  sumeq2i  15866  sum2id  15875  prodeq2i  16087  prod2id  16096  prdsbasex  17622  fnmrc  17782  sscpwex  17991  gsumwspan  19043  0frgp  19994  subdrgint  21061  frgpcyg  21880  psrbaglefi  22235  mvrf1  22294  mplmonmul  22346  elpt  23892  ptbasin2  23898  ptbasfi  23901  ptcld  23933  ptrescn  23959  xkoinjcn  24007  ptuncnv  24127  ptunhmeo  24128  itgfsum  26148  rolle  26311  dvlip  26314  dvivthlem1  26329  dvivth  26331  pserdv  26757  logtayl  26989  goeqi  32876  reuxfrdf  33088  psrmonmul  34183  sxbrsigalem0  34904  bnj852  35552  bnj1145  35624  tz9.1regs  35803  cvmsss2  36040  cvmliftphtlem  36083  dfon2lem1  36546  dfon2lem3  36548  dfon2lem7  36552  disjeq12i  36983  ptrest  38539  mblfinlem2  38578  voliunnfl  38584  sdclem2  38678  dmmzp  43745  arearect  44218  areaquad  44219  trclrelexplem  44712  corcltrcl  44740  cotrclrcl  44743  clsk3nimkb  45041  lhe4.4ex1a  45314  wfaxsep  45986  wfaxpow  45988  wfaxun  45990  dvcosax  46937  fourierdlem57  47174  fourierdlem58  47175  fourierdlem62  47179  nnsgrpnmnd  49276  elbigofrcl  49663  iunordi  50786