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 2140  ∀wral 3051

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

This theorem depends on definitions:  df-bi 197  df-ral 3056

This theorem is referenced by:  reximia  3148  rmoimia  3550  iuneq2i  4692  iineq2i  4693  dfiun2  4707  dfiin2  4708  eusv4  5027  reuxfr2d  5041  dfiun3  5536  dfiin3  5537  relmptopab  7050  ixpint  8104  noinfep  8733  tctr  8792  r1elssi  8844  ackbij2  9278  hsmexlem5  9465  axcc2lem  9471  inar1  9810  ccatalpha  13586  sumeq2i  14649  sum2id  14659  prodeq2i  14869  prod2id  14878  prdsbasex  16334  fnmrc  16490  sscpwex  16697  gsumwspan  17605  0frgp  18413  psrbaglefi  19595  mvrf1  19648  mplmonmul  19687  frgpcyg  20145  elpt  21598  ptbasin2  21604  ptbasfi  21607  ptcld  21639  ptrescn  21665  xkoinjcn  21713  ptuncnv  21833  ptunhmeo  21834  itgfsum  23813  rolle  23973  dvlip  23976  dvivthlem1  23991  dvivth  23993  pserdv  24403  logtayl  24627  goeqi  29463  reuxfr3d  29659  sxbrsigalem0  30664  bnj852  31320  bnj1145  31390  cvmsss2  31585  cvmliftphtlem  31628  dfon2lem1  32015  dfon2lem3  32017  dfon2lem7  32021  ptrest  33740  mblfinlem2  33779  voliunnfl  33785  sdclem2  33870  dmmzp  37817  arearect  38322  areaquad  38323  trclrelexplem  38524  corcltrcl  38552  cotrclrcl  38555  clsk3nimkb  38859  lhe4.4ex1a  39049  dvcosax  40663  fourierdlem57  40902  fourierdlem58  40903  fourierdlem62  40907  2reurmo  41707  nnsgrpnmnd  42347  elbigofrcl  42873  iunordi  42952