Theorem mprg 3058

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

Syntax hints:   → wi 4   ∈ wcel 2114  ∀wral 3052

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

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

This theorem is referenced by:  rmoimia  3688  reuxfrd  3695  2reurmo  3706  rabxm  4331  iuneq2i  4956  iineq2i  4957  dfiun2  4975  dfiin2  4976  eusv4  5349  dfiun3  5926  dfiin3  5927  relmptopab  7617  fsplitfpar  8068  ixpint  8873  noinfep  9581  tctr  9659  r1elssi  9729  ackbij2  10164  hsmexlem5  10352  axcc2lem  10358  inar1  10698  ccatalpha  14556  sumeq2i  15660  sum2id  15670  prodeq2i  15883  prod2id  15893  prdsbasex  17413  fnmrc  17573  sscpwex  17782  gsumwspan  18814  0frgp  19754  subdrgint  20780  frgpcyg  21553  psrbaglefi  21906  mvrf1  21964  mplmonmul  22014  elpt  23537  ptbasin2  23543  ptbasfi  23546  ptcld  23578  ptrescn  23604  xkoinjcn  23652  ptuncnv  23772  ptunhmeo  23773  itgfsum  25794  rolle  25957  dvlip  25960  dvivthlem1  25975  dvivth  25977  pserdv  26394  logtayl  26624  goeqi  32344  reuxfrdf  32560  psrmonmul  33694  sxbrsigalem0  34415  bnj852  35063  bnj1145  35135  tz9.1regs  35278  cvmsss2  35456  cvmliftphtlem  35499  dfon2lem1  35963  dfon2lem3  35965  dfon2lem7  35969  disjeq12i  36375  ptrest  37940  mblfinlem2  37979  voliunnfl  37985  sdclem2  38063  dmmzp  43165  arearect  43643  areaquad  43644  trclrelexplem  44138  corcltrcl  44166  cotrclrcl  44169  clsk3nimkb  44467  lhe4.4ex1a  44756  wfaxsep  45422  wfaxpow  45424  wfaxun  45426  dvcosax  46354  fourierdlem57  46591  fourierdlem58  46592  fourierdlem62  46596  nnsgrpnmnd  48648  elbigofrcl  49020  iunordi  50146