Theorem mprg 3073

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3067

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

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

This theorem is referenced by:  reximiaOLD  3094  rmoimia  3763  reuxfrd  3770  2reurmo  3781  rabxm  4413  ralf0  4537  iuneq2i  5036  iineq2i  5037  dfiun2  5056  dfiin2  5057  eusv4  5424  dfiun3  5992  dfiin3  5993  relmptopab  7700  fsplitfpar  8159  ixpint  8983  noinfep  9729  tctr  9809  r1elssi  9874  ackbij2  10311  hsmexlem5  10499  axcc2lem  10505  inar1  10844  ccatalpha  14641  sumeq2i  15746  sum2id  15756  prodeq2i  15966  prod2id  15976  prdsbasex  17510  fnmrc  17665  sscpwex  17876  gsumwspan  18881  0frgp  19821  subdrgint  20826  frgpcyg  21615  psrbaglefi  21969  mvrf1  22029  mplmonmul  22077  elpt  23601  ptbasin2  23607  ptbasfi  23610  ptcld  23642  ptrescn  23668  xkoinjcn  23716  ptuncnv  23836  ptunhmeo  23837  itgfsum  25882  rolle  26048  dvlip  26052  dvivthlem1  26067  dvivth  26069  pserdv  26491  logtayl  26720  goeqi  32305  reuxfrdf  32519  sxbrsigalem0  34236  bnj852  34897  bnj1145  34969  cvmsss2  35242  cvmliftphtlem  35285  dfon2lem1  35747  dfon2lem3  35749  dfon2lem7  35753  disjeq12i  36157  ptrest  37579  mblfinlem2  37618  voliunnfl  37624  sdclem2  37702  dmmzp  42689  arearect  43176  areaquad  43177  trclrelexplem  43673  corcltrcl  43701  cotrclrcl  43704  clsk3nimkb  44002  lhe4.4ex1a  44298  dvcosax  45847  fourierdlem57  46084  fourierdlem58  46085  fourierdlem62  46089  nnsgrpnmnd  47901  elbigofrcl  48284  iunordi  48769