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 2143  ∀wral 3077

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

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

This theorem is referenced by:  rmoimia  3705  reuxfrd  3712  2reurmo  3723  rabxm  4345  iuneq2i  4972  iineq2i  4973  dfiun2  4990  dfiin2  4991  eusv4  5364  dfiun3  5947  dfiin3  5948  relmptopab  7646  fsplitfpar  8097  ixpint  8907  noinfep  9613  tctr  9691  r1elssi  9761  ackbij2  10209  hsmexlem5  10398  axcc2lem  10404  inar1  10744  ccatalpha  14617  sgnrn  15121  sumeq2i  15735  sum2id  15745  prodeq2i  15958  prod2id  15968  prdsbasex  17489  fnmrc  17649  sscpwex  17858  gsumwspan  18890  0frgp  19829  subdrgint  20859  frgpcyg  21632  psrbaglefi  21985  mvrf1  22044  mplmonmul  22096  elpt  23639  ptbasin2  23645  ptbasfi  23648  ptcld  23680  ptrescn  23706  xkoinjcn  23754  ptuncnv  23874  ptunhmeo  23875  itgfsum  25896  rolle  26059  dvlip  26062  dvivthlem1  26077  dvivth  26079  pserdv  26499  logtayl  26732  goeqi  32483  reuxfrdf  32696  psrmonmul  33849  sxbrsigalem0  34570  bnj852  35218  bnj1145  35290  tz9.1regs  35434  cvmsss2  35629  cvmliftphtlem  35672  dfon2lem1  36136  dfon2lem3  36138  dfon2lem7  36142  disjeq12i  36558  ptrest  38123  mblfinlem2  38162  voliunnfl  38168  sdclem2  38246  dmmzp  43319  arearect  43797  areaquad  43798  trclrelexplem  44292  corcltrcl  44320  cotrclrcl  44323  clsk3nimkb  44621  lhe4.4ex1a  44896  wfaxsep  45562  wfaxpow  45564  wfaxun  45566  dvcosax  46491  fourierdlem57  46728  fourierdlem58  46729  fourierdlem62  46733  nnsgrpnmnd  48791  elbigofrcl  49163  iunordi  50289