Theorem mprg 3078

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

Syntax hints:   → wi 4   ∈ wcel 2106  ∀wral 3064

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

This theorem depends on definitions:  df-bi 206  df-ral 3069

This theorem is referenced by:  reximiaOLD  3177  rmoimia  3676  reuxfrd  3683  2reurmo  3694  ralf0  4444  iuneq2i  4945  iineq2i  4946  dfiun2  4963  dfiin2  4964  eusv4  5329  dfiun3  5875  dfiin3  5876  relmptopab  7519  fsplitfpar  7959  ixpint  8713  noinfep  9418  tctr  9498  r1elssi  9563  ackbij2  9999  hsmexlem5  10186  axcc2lem  10192  inar1  10531  ccatalpha  14298  sumeq2i  15411  sum2id  15420  prodeq2i  15629  prod2id  15638  prdsbasex  17161  fnmrc  17316  sscpwex  17527  gsumwspan  18485  0frgp  19385  subdrgint  20071  frgpcyg  20781  psrbaglefi  21135  psrbaglefiOLD  21136  mvrf1  21194  mplmonmul  21237  elpt  22723  ptbasin2  22729  ptbasfi  22732  ptcld  22764  ptrescn  22790  xkoinjcn  22838  ptuncnv  22958  ptunhmeo  22959  itgfsum  24991  rolle  25154  dvlip  25157  dvivthlem1  25172  dvivth  25174  pserdv  25588  logtayl  25815  goeqi  30635  reuxfrdf  30839  sxbrsigalem0  32238  bnj852  32901  bnj1145  32973  cvmsss2  33236  cvmliftphtlem  33279  dfon2lem1  33759  dfon2lem3  33761  dfon2lem7  33765  ptrest  35776  mblfinlem2  35815  voliunnfl  35821  sdclem2  35900  dmmzp  40555  arearect  41046  areaquad  41047  trclrelexplem  41319  corcltrcl  41347  cotrclrcl  41350  clsk3nimkb  41650  lhe4.4ex1a  41947  dvcosax  43467  fourierdlem57  43704  fourierdlem58  43705  fourierdlem62  43709  nnsgrpnmnd  45372  elbigofrcl  45896  iunordi  46383