Theorem mprg 2910

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

Syntax hints:   → wi 4   ∈ wcel 1977  ∀wral 2896

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

This theorem depends on definitions:  df-bi 196  df-ral 2901

This theorem is referenced by:  reximia  2992  rmoimia  3375  iuneq2i  4475  iineq2i  4476  dfiun2  4490  dfiin2  4491  eusv4  4803  reuxfr2d  4817  dfiun3  5301  dfiin3  5302  relmptopab  6781  ixpint  7821  noinfep  8440  tctr  8499  r1elssi  8551  ackbij2  8948  hsmexlem5  9135  axcc2lem  9141  inar1  9476  ccatalpha  13228  sumeq2i  14277  sum2id  14286  prodeq2i  14488  prod2id  14497  prdsbasex  15934  fnmrc  16090  sscpwex  16298  gsumwspan  17206  0frgp  18015  psrbaglefi  19193  mvrf1  19246  mplmonmul  19285  frgpcyg  19741  elpt  21185  ptbasin2  21191  ptbasfi  21194  ptcld  21226  ptrescn  21252  xkoinjcn  21300  ptuncnv  21420  ptunhmeo  21421  itgfsum  23399  rolle  23557  dvlip  23560  dvivthlem1  23575  dvivth  23577  pserdv  23987  logtayl  24206  goeqi  28516  reuxfr3d  28713  sxbrsigalem0  29660  bnj852  30245  bnj1145  30315  cvmsss2  30510  cvmliftphtlem  30553  dfon2lem1  30932  dfon2lem3  30934  dfon2lem7  30938  ptrest  32578  mblfinlem2  32617  voliunnfl  32623  sdclem2  32708  dmmzp  36314  arearect  36820  areaquad  36821  trclrelexplem  37022  corcltrcl  37050  cotrclrcl  37053  clsk3nimkb  37358  lhe4.4ex1a  37550  dvcosax  38816  fourierdlem57  39056  fourierdlem58  39057  fourierdlem62  39061  2reurmo  39831  nnsgrpnmnd  41608  elbigofrcl  42142  iunordi  42221