Theorem mprg 3084

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142  ∀wral 3078

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

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

This theorem is used by:  rmoimia  3703  reuxfrd  3710  2reurmo  3721  rabxm  4346  iuneq2i  4977  iineq2i  4978  dfiun2  4995  dfiin2  4996  eusv4  5376  dfiun3  5959  dfiin3  5960  relmptopab  7662  fsplitfpar  8111  ixpint  8921  noinfep  9627  tctr  9705  r1elssi  9775  ackbij2  10232  hsmexlem5  10420  axcc2lem  10426  inar1  10766  ccatalpha  14638  sgnrn  15142  sumeq2i  15756  sum2id  15766  prodeq2i  15979  prod2id  15989  prdsbasex  17509  fnmrc  17669  sscpwex  17878  gsumwspan  18911  0frgp  19855  subdrgint  20917  frgpcyg  21734  psrbaglefi  22087  mvrf1  22146  mplmonmul  22198  elpt  23740  ptbasin2  23746  ptbasfi  23749  ptcld  23781  ptrescn  23807  xkoinjcn  23855  ptuncnv  23975  ptunhmeo  23976  itgfsum  25997  rolle  26160  dvlip  26163  dvivthlem1  26178  dvivth  26180  pserdv  26603  logtayl  26836  goeqi  32636  reuxfrdf  32848  psrmonmul  33949  sxbrsigalem0  34670  bnj852  35318  bnj1145  35390  tz9.1regs  35555  cvmsss2  35774  cvmliftphtlem  35817  dfon2lem1  36281  dfon2lem3  36283  dfon2lem7  36287  disjeq12i  36733  ptrest  38298  mblfinlem2  38337  voliunnfl  38343  sdclem2  38421  dmmzp  43492  arearect  43970  areaquad  43971  trclrelexplem  44465  corcltrcl  44493  cotrclrcl  44496  clsk3nimkb  44794  lhe4.4ex1a  45067  wfaxsep  45732  wfaxpow  45734  wfaxun  45736  dvcosax  46668  fourierdlem57  46905  fourierdlem58  46906  fourierdlem62  46910  nnsgrpnmnd  48971  elbigofrcl  49358  iunordi  50483  crossp3i  50676