Theorem mprg 3055

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

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

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 3050

This theorem is referenced by:  rmoimia  3684  reuxfrd  3691  2reurmo  3702  rabxm  4320  iuneq2i  4945  iineq2i  4946  dfiun2  4963  dfiin2  4964  eusv4  5337  dfiun3  5914  dfiin3  5915  relmptopab  7606  fsplitfpar  8057  ixpint  8862  noinfep  9570  tctr  9648  r1elssi  9718  ackbij2  10153  hsmexlem5  10341  axcc2lem  10347  inar1  10687  ccatalpha  14545  sumeq2i  15649  sum2id  15659  prodeq2i  15872  prod2id  15882  prdsbasex  17402  fnmrc  17562  sscpwex  17771  gsumwspan  18803  0frgp  19743  subdrgint  20769  frgpcyg  21542  psrbaglefi  21895  mvrf1  21953  mplmonmul  22003  elpt  23525  ptbasin2  23531  ptbasfi  23534  ptcld  23566  ptrescn  23592  xkoinjcn  23640  ptuncnv  23760  ptunhmeo  23761  itgfsum  25782  rolle  25945  dvlip  25948  dvivthlem1  25963  dvivth  25965  pserdv  26382  logtayl  26612  goeqi  32332  reuxfrdf  32548  psrmonmul  33682  sxbrsigalem0  34403  bnj852  35051  bnj1145  35123  tz9.1regs  35266  cvmsss2  35444  cvmliftphtlem  35487  dfon2lem1  35951  dfon2lem3  35953  dfon2lem7  35957  disjeq12i  36363  ptrest  37928  mblfinlem2  37967  voliunnfl  37973  sdclem2  38051  dmmzp  43153  arearect  43631  areaquad  43632  trclrelexplem  44126  corcltrcl  44154  cotrclrcl  44157  clsk3nimkb  44455  lhe4.4ex1a  44744  wfaxsep  45410  wfaxpow  45412  wfaxun  45414  dvcosax  46342  fourierdlem57  46579  fourierdlem58  46580  fourierdlem62  46584  nnsgrpnmnd  48642  elbigofrcl  49014  iunordi  50140