Theorem mprg 3058

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

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

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 3053

This theorem is referenced by:  rmoimia  3688  reuxfrd  3695  2reurmo  3706  rabxm  4331  iuneq2i  4956  iineq2i  4957  dfiun2  4975  dfiin2  4976  eusv4  5341  dfiun3  5917  dfiin3  5918  relmptopab  7608  fsplitfpar  8059  ixpint  8864  noinfep  9570  tctr  9648  r1elssi  9718  ackbij2  10153  hsmexlem5  10341  axcc2lem  10347  inar1  10687  ccatalpha  14518  sumeq2i  15622  sum2id  15632  prodeq2i  15842  prod2id  15852  prdsbasex  17371  fnmrc  17531  sscpwex  17740  gsumwspan  18772  0frgp  19712  subdrgint  20738  frgpcyg  21530  psrbaglefi  21883  mvrf1  21942  mplmonmul  21992  elpt  23515  ptbasin2  23521  ptbasfi  23524  ptcld  23556  ptrescn  23582  xkoinjcn  23630  ptuncnv  23750  ptunhmeo  23751  itgfsum  25772  rolle  25935  dvlip  25939  dvivthlem1  25954  dvivth  25956  pserdv  26379  logtayl  26609  goeqi  32333  reuxfrdf  32549  psrmonmul  33699  sxbrsigalem0  34421  bnj852  35069  bnj1145  35141  tz9.1regs  35284  cvmsss2  35462  cvmliftphtlem  35505  dfon2lem1  35969  dfon2lem3  35971  dfon2lem7  35975  disjeq12i  36381  ptrest  37931  mblfinlem2  37970  voliunnfl  37976  sdclem2  38054  dmmzp  43164  arearect  43646  areaquad  43647  trclrelexplem  44141  corcltrcl  44169  cotrclrcl  44172  clsk3nimkb  44470  lhe4.4ex1a  44759  wfaxsep  45425  wfaxpow  45427  wfaxun  45429  dvcosax  46358  fourierdlem57  46595  fourierdlem58  46596  fourierdlem62  46600  nnsgrpnmnd  48612  elbigofrcl  48984  iunordi  50110