Theorem mprg 3057

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

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

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 3052

This theorem is referenced by:  rmoimia  3724  reuxfrd  3731  2reurmo  3742  rabxm  4365  ralf0  4489  iuneq2i  4989  iineq2i  4990  dfiun2  5009  dfiin2  5010  eusv4  5376  dfiun3  5949  dfiin3  5950  relmptopab  7657  fsplitfpar  8117  ixpint  8939  noinfep  9674  tctr  9754  r1elssi  9819  ackbij2  10256  hsmexlem5  10444  axcc2lem  10450  inar1  10789  ccatalpha  14611  sumeq2i  15714  sum2id  15724  prodeq2i  15934  prod2id  15944  prdsbasex  17464  fnmrc  17619  sscpwex  17828  gsumwspan  18824  0frgp  19760  subdrgint  20763  frgpcyg  21534  psrbaglefi  21886  mvrf1  21946  mplmonmul  21994  elpt  23510  ptbasin2  23516  ptbasfi  23519  ptcld  23551  ptrescn  23577  xkoinjcn  23625  ptuncnv  23745  ptunhmeo  23746  itgfsum  25780  rolle  25946  dvlip  25950  dvivthlem1  25965  dvivth  25967  pserdv  26391  logtayl  26621  goeqi  32254  reuxfrdf  32472  sxbrsigalem0  34303  bnj852  34952  bnj1145  35024  cvmsss2  35296  cvmliftphtlem  35339  dfon2lem1  35801  dfon2lem3  35803  dfon2lem7  35807  disjeq12i  36211  ptrest  37643  mblfinlem2  37682  voliunnfl  37688  sdclem2  37766  dmmzp  42756  arearect  43239  areaquad  43240  trclrelexplem  43735  corcltrcl  43763  cotrclrcl  43766  clsk3nimkb  44064  lhe4.4ex1a  44353  wfaxsep  45020  wfaxpow  45022  wfaxun  45024  dvcosax  45955  fourierdlem57  46192  fourierdlem58  46193  fourierdlem62  46197  nnsgrpnmnd  48153  elbigofrcl  48530  iunordi  49541