Theorem mprg 3065

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3059

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792

This theorem depends on definitions:  df-bi 207  df-ral 3060

This theorem is referenced by:  reximiaOLD  3086  rmoimia  3750  reuxfrd  3757  2reurmo  3768  rabxm  4396  ralf0  4520  iuneq2i  5018  iineq2i  5019  dfiun2  5038  dfiin2  5039  eusv4  5412  dfiun3  5983  dfiin3  5984  relmptopab  7683  fsplitfpar  8142  ixpint  8964  noinfep  9698  tctr  9778  r1elssi  9843  ackbij2  10280  hsmexlem5  10468  axcc2lem  10474  inar1  10813  ccatalpha  14628  sumeq2i  15731  sum2id  15741  prodeq2i  15951  prod2id  15961  prdsbasex  17497  fnmrc  17652  sscpwex  17863  gsumwspan  18872  0frgp  19812  subdrgint  20821  frgpcyg  21610  psrbaglefi  21964  mvrf1  22024  mplmonmul  22072  elpt  23596  ptbasin2  23602  ptbasfi  23605  ptcld  23637  ptrescn  23663  xkoinjcn  23711  ptuncnv  23831  ptunhmeo  23832  itgfsum  25877  rolle  26043  dvlip  26047  dvivthlem1  26062  dvivth  26064  pserdv  26488  logtayl  26717  goeqi  32302  reuxfrdf  32519  sxbrsigalem0  34253  bnj852  34914  bnj1145  34986  cvmsss2  35259  cvmliftphtlem  35302  dfon2lem1  35765  dfon2lem3  35767  dfon2lem7  35771  disjeq12i  36175  ptrest  37606  mblfinlem2  37645  voliunnfl  37651  sdclem2  37729  dmmzp  42721  arearect  43204  areaquad  43205  trclrelexplem  43701  corcltrcl  43729  cotrclrcl  43732  clsk3nimkb  44030  lhe4.4ex1a  44325  wfaxsep  44951  dvcosax  45882  fourierdlem57  46119  fourierdlem58  46120  fourierdlem62  46124  nnsgrpnmnd  48022  elbigofrcl  48400  iunordi  48908