Theorem mprg 3086

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147  ∀wral 3080

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 3081

This theorem is used by:  rmoimia  3702  reuxfrd  3709  2reurmo  3720  rabxm  4343  iuneq2i  4976  iineq2i  4977  dfiun2  4993  dfiin2  4994  eusv4  5372  dfiun3  5959  dfiin3  5960  relmptopab  7695  fsplitfpar  8156  ixpint  8981  noinfep  9688  tctr  9766  r1elssi  9840  ackbij2  10347  hsmexlem5  10535  axcc2lem  10541  inar1  10887  ccatalpha  14767  sgnrn  15280  sumeq2i  15894  sum2id  15903  prodeq2i  16115  prod2id  16124  prdsbasex  17650  fnmrc  17810  sscpwex  18019  gsumwspan  19071  0frgp  20023  subdrgint  21090  frgpcyg  21909  psrbaglefi  22264  mvrf1  22323  mplmonmul  22375  elpt  23921  ptbasin2  23927  ptbasfi  23930  ptcld  23962  ptrescn  23988  xkoinjcn  24036  ptuncnv  24156  ptunhmeo  24157  itgfsum  26177  rolle  26340  dvlip  26343  dvivthlem1  26358  dvivth  26360  pserdv  26786  logtayl  27018  goeqi  32905  reuxfrdf  33159  psrmonmul  34252  sxbrsigalem0  34973  bnj852  35621  bnj1145  35693  tz9.1regs  35902  cvmsss2  36206  cvmliftphtlem  36249  dfon2lem1  36723  dfon2lem3  36725  dfon2lem7  36729  disjeq12i  37160  ptrest  38729  mblfinlem2  38768  voliunnfl  38774  sdclem2  38868  dmmzp  43937  arearect  44409  areaquad  44410  trclrelexplem  44903  corcltrcl  44931  cotrclrcl  44934  clsk3nimkb  45232  lhe4.4ex1a  45505  wfaxsep  46180  wfaxpow  46182  wfaxun  46184  dvcosax  47141  fourierdlem57  47378  fourierdlem58  47379  fourierdlem62  47383  nnsgrpnmnd  49480  elbigofrcl  49867  iunordi  51065