Theorem mprg 3083

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

Syntax hints:   → wi 4   ∈ wcel 2141  ∀wral 3077

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823

This theorem depends on definitions:  df-bi 210  df-ral 3078

This theorem is referenced by:  rmoimia  3703  reuxfrd  3710  2reurmo  3721  rabxm  4346  iuneq2i  4977  iineq2i  4978  dfiun2  4995  dfiin2  4996  eusv4  5377  dfiun3  5960  dfiin3  5961  relmptopab  7660  fsplitfpar  8112  ixpint  8922  noinfep  9628  tctr  9706  r1elssi  9776  ackbij2  10224  hsmexlem5  10413  axcc2lem  10419  inar1  10759  ccatalpha  14630  sgnrn  15134  sumeq2i  15748  sum2id  15758  prodeq2i  15971  prod2id  15981  prdsbasex  17502  fnmrc  17662  sscpwex  17871  gsumwspan  18904  0frgp  19848  subdrgint  20885  frgpcyg  21702  psrbaglefi  22055  mvrf1  22114  mplmonmul  22166  elpt  23708  ptbasin2  23714  ptbasfi  23717  ptcld  23749  ptrescn  23775  xkoinjcn  23823  ptuncnv  23943  ptunhmeo  23944  itgfsum  25965  rolle  26128  dvlip  26131  dvivthlem1  26146  dvivth  26148  pserdv  26568  logtayl  26801  goeqi  32591  reuxfrdf  32803  psrmonmul  33906  sxbrsigalem0  34627  bnj852  35275  bnj1145  35347  tz9.1regs  35501  cvmsss2  35720  cvmliftphtlem  35763  dfon2lem1  36227  dfon2lem3  36229  dfon2lem7  36233  disjeq12i  36649  ptrest  38214  mblfinlem2  38253  voliunnfl  38259  sdclem2  38337  dmmzp  43412  arearect  43890  areaquad  43891  trclrelexplem  44385  corcltrcl  44413  cotrclrcl  44416  clsk3nimkb  44714  lhe4.4ex1a  44987  wfaxsep  45652  wfaxpow  45654  wfaxun  45656  dvcosax  46588  fourierdlem57  46825  fourierdlem58  46826  fourierdlem62  46830  nnsgrpnmnd  48888  elbigofrcl  49275  iunordi  50400