Theorem mprg 3050

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3044

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 3045

This theorem is referenced by:  rmoimia  3712  reuxfrd  3719  2reurmo  3730  rabxm  4353  ralf0  4477  iuneq2i  4977  iineq2i  4978  dfiun2  4997  dfiin2  4998  eusv4  5361  dfiun3  5933  dfiin3  5934  relmptopab  7639  fsplitfpar  8097  ixpint  8898  noinfep  9613  tctr  9693  r1elssi  9758  ackbij2  10195  hsmexlem5  10383  axcc2lem  10389  inar1  10728  ccatalpha  14558  sumeq2i  15664  sum2id  15674  prodeq2i  15884  prod2id  15894  prdsbasex  17413  fnmrc  17568  sscpwex  17777  gsumwspan  18773  0frgp  19709  subdrgint  20712  frgpcyg  21483  psrbaglefi  21835  mvrf1  21895  mplmonmul  21943  elpt  23459  ptbasin2  23465  ptbasfi  23468  ptcld  23500  ptrescn  23526  xkoinjcn  23574  ptuncnv  23694  ptunhmeo  23695  itgfsum  25728  rolle  25894  dvlip  25898  dvivthlem1  25913  dvivth  25915  pserdv  26339  logtayl  26569  goeqi  32202  reuxfrdf  32420  sxbrsigalem0  34262  bnj852  34911  bnj1145  34983  cvmsss2  35261  cvmliftphtlem  35304  dfon2lem1  35771  dfon2lem3  35773  dfon2lem7  35777  disjeq12i  36181  ptrest  37613  mblfinlem2  37652  voliunnfl  37658  sdclem2  37736  dmmzp  42721  arearect  43204  areaquad  43205  trclrelexplem  43700  corcltrcl  43728  cotrclrcl  43731  clsk3nimkb  44029  lhe4.4ex1a  44318  wfaxsep  44985  wfaxpow  44987  wfaxun  44989  dvcosax  45924  fourierdlem57  46161  fourierdlem58  46162  fourierdlem62  46166  nnsgrpnmnd  48166  elbigofrcl  48539  iunordi  49666