Theorem mprg 3072

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

Syntax hints:   → wi 4   ∈ wcel 2132  ∀wral 3066

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

This theorem depends on definitions:  df-bi 209  df-ral 3067

This theorem is referenced by:  rmoimia  3694  reuxfrd  3701  2reurmo  3712  rabxm  4334  iuneq2i  4961  iineq2i  4962  dfiun2  4979  dfiin2  4980  eusv4  5353  dfiun3  5935  dfiin3  5936  relmptopab  7631  fsplitfpar  8081  ixpint  8892  noinfep  9601  tctr  9679  r1elssi  9749  ackbij2  10184  hsmexlem5  10373  axcc2lem  10379  inar1  10719  ccatalpha  14593  sumeq2i  15697  sum2id  15707  prodeq2i  15920  prod2id  15930  prdsbasex  17451  fnmrc  17611  sscpwex  17820  gsumwspan  18852  0frgp  19791  subdrgint  20821  frgpcyg  21594  psrbaglefi  21947  mvrf1  22006  mplmonmul  22058  elpt  23601  ptbasin2  23607  ptbasfi  23610  ptcld  23642  ptrescn  23668  xkoinjcn  23716  ptuncnv  23836  ptunhmeo  23837  itgfsum  25858  rolle  26021  dvlip  26024  dvivthlem1  26039  dvivth  26041  pserdv  26458  logtayl  26691  goeqi  32411  reuxfrdf  32627  psrmonmul  33791  sxbrsigalem0  34512  bnj852  35163  bnj1145  35235  tz9.1regs  35375  cvmsss2  35562  cvmliftphtlem  35605  dfon2lem1  36069  dfon2lem3  36071  dfon2lem7  36075  disjeq12i  36491  ptrest  38056  mblfinlem2  38095  voliunnfl  38101  sdclem2  38179  dmmzp  43252  arearect  43730  areaquad  43731  trclrelexplem  44225  corcltrcl  44253  cotrclrcl  44256  clsk3nimkb  44554  lhe4.4ex1a  44843  wfaxsep  45509  wfaxpow  45511  wfaxun  45513  dvcosax  46438  fourierdlem57  46675  fourierdlem58  46676  fourierdlem62  46680  nnsgrpnmnd  48738  elbigofrcl  49110  iunordi  50236