Theorem mprg 3068

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  reximiaOLD  3089  rmoimia  3737  reuxfrd  3744  2reurmo  3755  ralf0  4513  iuneq2i  5018  iineq2i  5019  dfiun2  5036  dfiin2  5037  eusv4  5404  dfiun3  5964  dfiin3  5965  relmptopab  7653  fsplitfpar  8101  ixpint  8916  noinfep  9652  tctr  9732  r1elssi  9797  ackbij2  10235  hsmexlem5  10422  axcc2lem  10428  inar1  10767  ccatalpha  14540  sumeq2i  15642  sum2id  15651  prodeq2i  15860  prod2id  15869  prdsbasex  17393  fnmrc  17548  sscpwex  17759  gsumwspan  18724  0frgp  19642  subdrgint  20412  frgpcyg  21121  psrbaglefi  21477  psrbaglefiOLD  21478  mvrf1  21537  mplmonmul  21583  elpt  23068  ptbasin2  23074  ptbasfi  23077  ptcld  23109  ptrescn  23135  xkoinjcn  23183  ptuncnv  23303  ptunhmeo  23304  itgfsum  25336  rolle  25499  dvlip  25502  dvivthlem1  25517  dvivth  25519  pserdv  25933  logtayl  26160  goeqi  31514  reuxfrdf  31719  sxbrsigalem0  33259  bnj852  33921  bnj1145  33993  cvmsss2  34254  cvmliftphtlem  34297  dfon2lem1  34744  dfon2lem3  34746  dfon2lem7  34750  ptrest  36476  mblfinlem2  36515  voliunnfl  36521  sdclem2  36599  dmmzp  41457  arearect  41950  areaquad  41951  trclrelexplem  42448  corcltrcl  42476  cotrclrcl  42479  clsk3nimkb  42777  lhe4.4ex1a  43074  dvcosax  44629  fourierdlem57  44866  fourierdlem58  44867  fourierdlem62  44871  nnsgrpnmnd  46575  elbigofrcl  47190  iunordi  47676