Theorem mprg 3055

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

Syntax hints:   → wi 4   ∈ wcel 2113  ∀wral 3049

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

This theorem depends on definitions:  df-bi 207  df-ral 3050

This theorem is referenced by:  rmoimia  3697  reuxfrd  3704  2reurmo  3715  rabxm  4341  ralf0  4465  iuneq2i  4965  iineq2i  4966  dfiun2  4984  dfiin2  4985  eusv4  5348  dfiun3  5916  dfiin3  5917  relmptopab  7605  fsplitfpar  8057  ixpint  8858  noinfep  9560  tctr  9638  r1elssi  9708  ackbij2  10143  hsmexlem5  10331  axcc2lem  10337  inar1  10676  ccatalpha  14511  sumeq2i  15615  sum2id  15625  prodeq2i  15835  prod2id  15845  prdsbasex  17364  fnmrc  17523  sscpwex  17732  gsumwspan  18764  0frgp  19701  subdrgint  20728  frgpcyg  21520  psrbaglefi  21873  mvrf1  21933  mplmonmul  21981  elpt  23497  ptbasin2  23503  ptbasfi  23506  ptcld  23538  ptrescn  23564  xkoinjcn  23612  ptuncnv  23732  ptunhmeo  23733  itgfsum  25765  rolle  25931  dvlip  25935  dvivthlem1  25950  dvivth  25952  pserdv  26376  logtayl  26606  goeqi  32264  reuxfrdf  32481  sxbrsigalem0  34295  bnj852  34944  bnj1145  35016  tz9.1regs  35141  cvmsss2  35329  cvmliftphtlem  35372  dfon2lem1  35836  dfon2lem3  35838  dfon2lem7  35842  disjeq12i  36248  ptrest  37669  mblfinlem2  37708  voliunnfl  37714  sdclem2  37792  dmmzp  42840  arearect  43322  areaquad  43323  trclrelexplem  43818  corcltrcl  43846  cotrclrcl  43849  clsk3nimkb  44147  lhe4.4ex1a  44436  wfaxsep  45102  wfaxpow  45104  wfaxun  45106  dvcosax  46038  fourierdlem57  46275  fourierdlem58  46276  fourierdlem62  46280  nnsgrpnmnd  48292  elbigofrcl  48665  iunordi  49792