Theorem mprg 3084

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3070

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 210  df-ral 3075

This theorem is referenced by:  reximia  3170  rmoimia  3655  reuxfrd  3662  2reurmo  3674  ralf0  4406  iuneq2i  4904  iineq2i  4905  dfiun2  4922  dfiin2  4923  eusv4  5275  dfiun3  5807  dfiin3  5808  relmptopab  7391  fsplitfpar  7819  ixpint  8507  noinfep  9156  tctr  9215  r1elssi  9267  ackbij2  9703  hsmexlem5  9890  axcc2lem  9896  inar1  10235  ccatalpha  13994  sumeq2i  15104  sum2id  15113  prodeq2i  15321  prod2id  15330  prdsbasex  16782  fnmrc  16936  sscpwex  17144  gsumwspan  18077  0frgp  18972  subdrgint  19650  frgpcyg  20341  psrbaglefi  20694  psrbaglefiOLD  20695  mvrf1  20753  mplmonmul  20796  elpt  22272  ptbasin2  22278  ptbasfi  22281  ptcld  22313  ptrescn  22339  xkoinjcn  22387  ptuncnv  22507  ptunhmeo  22508  itgfsum  24526  rolle  24689  dvlip  24692  dvivthlem1  24707  dvivth  24709  pserdv  25123  logtayl  25350  goeqi  30155  reuxfrdf  30361  sxbrsigalem0  31757  bnj852  32421  bnj1145  32493  cvmsss2  32752  cvmliftphtlem  32795  dfon2lem1  33275  dfon2lem3  33277  dfon2lem7  33281  ptrest  35336  mblfinlem2  35375  voliunnfl  35381  sdclem2  35460  dmmzp  40047  arearect  40538  areaquad  40539  trclrelexplem  40785  corcltrcl  40813  cotrclrcl  40816  clsk3nimkb  41116  lhe4.4ex1a  41406  dvcosax  42934  fourierdlem57  43171  fourierdlem58  43172  fourierdlem62  43176  nnsgrpnmnd  44805  elbigofrcl  45329  iunordi  45598