Theorem mprg 3051

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

Syntax hints:   → wi 4   ∈ wcel 2110  ∀wral 3045

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

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

This theorem is referenced by:  rmoimia  3698  reuxfrd  3705  2reurmo  3716  rabxm  4338  ralf0  4462  iuneq2i  4961  iineq2i  4962  dfiun2  4980  dfiin2  4981  eusv4  5342  dfiun3  5906  dfiin3  5907  relmptopab  7591  fsplitfpar  8043  ixpint  8844  noinfep  9545  tctr  9625  r1elssi  9690  ackbij2  10125  hsmexlem5  10313  axcc2lem  10319  inar1  10658  ccatalpha  14493  sumeq2i  15597  sum2id  15607  prodeq2i  15817  prod2id  15827  prdsbasex  17346  fnmrc  17505  sscpwex  17714  gsumwspan  18746  0frgp  19684  subdrgint  20711  frgpcyg  21503  psrbaglefi  21856  mvrf1  21916  mplmonmul  21964  elpt  23480  ptbasin2  23486  ptbasfi  23489  ptcld  23521  ptrescn  23547  xkoinjcn  23595  ptuncnv  23715  ptunhmeo  23716  itgfsum  25748  rolle  25914  dvlip  25918  dvivthlem1  25933  dvivth  25935  pserdv  26359  logtayl  26589  goeqi  32243  reuxfrdf  32460  sxbrsigalem0  34274  bnj852  34923  bnj1145  34995  tz9.1regs  35102  cvmsss2  35286  cvmliftphtlem  35329  dfon2lem1  35796  dfon2lem3  35798  dfon2lem7  35802  disjeq12i  36206  ptrest  37638  mblfinlem2  37677  voliunnfl  37683  sdclem2  37761  dmmzp  42745  arearect  43227  areaquad  43228  trclrelexplem  43723  corcltrcl  43751  cotrclrcl  43754  clsk3nimkb  44052  lhe4.4ex1a  44341  wfaxsep  45007  wfaxpow  45009  wfaxun  45011  dvcosax  45943  fourierdlem57  46180  fourierdlem58  46181  fourierdlem62  46185  nnsgrpnmnd  48188  elbigofrcl  48561  iunordi  49688