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  3700  reuxfrd  3707  2reurmo  3718  rabxm  4343  iuneq2i  4969  iineq2i  4970  dfiun2  4988  dfiin2  4989  eusv4  5352  dfiun3  5920  dfiin3  5921  relmptopab  7611  fsplitfpar  8063  ixpint  8868  noinfep  9574  tctr  9652  r1elssi  9722  ackbij2  10157  hsmexlem5  10345  axcc2lem  10351  inar1  10691  ccatalpha  14522  sumeq2i  15626  sum2id  15636  prodeq2i  15846  prod2id  15856  prdsbasex  17375  fnmrc  17535  sscpwex  17744  gsumwspan  18776  0frgp  19713  subdrgint  20741  frgpcyg  21533  psrbaglefi  21887  mvrf1  21946  mplmonmul  21996  elpt  23521  ptbasin2  23527  ptbasfi  23530  ptcld  23562  ptrescn  23588  xkoinjcn  23636  ptuncnv  23756  ptunhmeo  23757  itgfsum  25789  rolle  25955  dvlip  25959  dvivthlem1  25974  dvivth  25976  pserdv  26400  logtayl  26630  goeqi  32353  reuxfrdf  32569  psrmonmul  33719  sxbrsigalem0  34441  bnj852  35090  bnj1145  35162  tz9.1regs  35303  cvmsss2  35481  cvmliftphtlem  35524  dfon2lem1  35988  dfon2lem3  35990  dfon2lem7  35994  disjeq12i  36400  ptrest  37833  mblfinlem2  37872  voliunnfl  37878  sdclem2  37956  dmmzp  43053  arearect  43535  areaquad  43536  trclrelexplem  44030  corcltrcl  44058  cotrclrcl  44061  clsk3nimkb  44359  lhe4.4ex1a  44648  wfaxsep  45314  wfaxpow  45316  wfaxun  45318  dvcosax  46247  fourierdlem57  46484  fourierdlem58  46485  fourierdlem62  46489  nnsgrpnmnd  48501  elbigofrcl  48873  iunordi  49999