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  7610  fsplitfpar  8062  ixpint  8867  noinfep  9573  tctr  9651  r1elssi  9721  ackbij2  10156  hsmexlem5  10344  axcc2lem  10350  inar1  10690  ccatalpha  14521  sumeq2i  15625  sum2id  15635  prodeq2i  15845  prod2id  15855  prdsbasex  17374  fnmrc  17534  sscpwex  17743  gsumwspan  18775  0frgp  19712  subdrgint  20740  frgpcyg  21532  psrbaglefi  21886  mvrf1  21945  mplmonmul  21995  elpt  23520  ptbasin2  23526  ptbasfi  23529  ptcld  23561  ptrescn  23587  xkoinjcn  23635  ptuncnv  23755  ptunhmeo  23756  itgfsum  25788  rolle  25954  dvlip  25958  dvivthlem1  25973  dvivth  25975  pserdv  26399  logtayl  26629  goeqi  32331  reuxfrdf  32547  sxbrsigalem0  34409  bnj852  35058  bnj1145  35130  tz9.1regs  35271  cvmsss2  35449  cvmliftphtlem  35492  dfon2lem1  35956  dfon2lem3  35958  dfon2lem7  35962  disjeq12i  36368  ptrest  37791  mblfinlem2  37830  voliunnfl  37836  sdclem2  37914  dmmzp  43011  arearect  43493  areaquad  43494  trclrelexplem  43988  corcltrcl  44016  cotrclrcl  44019  clsk3nimkb  44317  lhe4.4ex1a  44606  wfaxsep  45272  wfaxpow  45274  wfaxun  45276  dvcosax  46206  fourierdlem57  46443  fourierdlem58  46444  fourierdlem62  46448  nnsgrpnmnd  48460  elbigofrcl  48832  iunordi  49958