Theorem mprg 3067

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

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

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

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

This theorem is referenced by:  reximiaOLD  3088  rmoimia  3747  reuxfrd  3754  2reurmo  3765  rabxm  4390  ralf0  4514  iuneq2i  5013  iineq2i  5014  dfiun2  5033  dfiin2  5034  eusv4  5406  dfiun3  5980  dfiin3  5981  relmptopab  7683  fsplitfpar  8143  ixpint  8965  noinfep  9700  tctr  9780  r1elssi  9845  ackbij2  10282  hsmexlem5  10470  axcc2lem  10476  inar1  10815  ccatalpha  14631  sumeq2i  15734  sum2id  15744  prodeq2i  15954  prod2id  15964  prdsbasex  17495  fnmrc  17650  sscpwex  17859  gsumwspan  18859  0frgp  19797  subdrgint  20804  frgpcyg  21592  psrbaglefi  21946  mvrf1  22006  mplmonmul  22054  elpt  23580  ptbasin2  23586  ptbasfi  23589  ptcld  23621  ptrescn  23647  xkoinjcn  23695  ptuncnv  23815  ptunhmeo  23816  itgfsum  25862  rolle  26028  dvlip  26032  dvivthlem1  26047  dvivth  26049  pserdv  26473  logtayl  26702  goeqi  32292  reuxfrdf  32510  sxbrsigalem0  34273  bnj852  34935  bnj1145  35007  cvmsss2  35279  cvmliftphtlem  35322  dfon2lem1  35784  dfon2lem3  35786  dfon2lem7  35790  disjeq12i  36194  ptrest  37626  mblfinlem2  37665  voliunnfl  37671  sdclem2  37749  dmmzp  42744  arearect  43227  areaquad  43228  trclrelexplem  43724  corcltrcl  43752  cotrclrcl  43755  clsk3nimkb  44053  lhe4.4ex1a  44348  wfaxsep  45012  wfaxpow  45014  wfaxun  45016  dvcosax  45941  fourierdlem57  46178  fourierdlem58  46179  fourierdlem62  46183  nnsgrpnmnd  48094  elbigofrcl  48471  iunordi  49196