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 ⊢ 𝜓

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  rmoimia  3702  reuxfrd  3709  2reurmo  3720  rabxm  4343  iuneq2i  4976  iineq2i  4977  dfiun2  4994  dfiin2  4995  eusv4  5375  dfiun3  5958  dfiin3  5959  relmptopab  7667  fsplitfpar  8118  ixpint  8935  noinfep  9642  tctr  9720  r1elssi  9790  ackbij2  10247  hsmexlem5  10435  axcc2lem  10441  inar1  10787  ccatalpha  14662  sgnrn  15173  sumeq2i  15787  sum2id  15796  prodeq2i  16009  prod2id  16019  prdsbasex  17539  fnmrc  17699  sscpwex  17908  gsumwspan  18956  0frgp  19907  subdrgint  20970  frgpcyg  21787  psrbaglefi  22142  mvrf1  22201  mplmonmul  22253  elpt  23799  ptbasin2  23805  ptbasfi  23808  ptcld  23840  ptrescn  23866  xkoinjcn  23914  ptuncnv  24034  ptunhmeo  24035  itgfsum  26056  rolle  26219  dvlip  26222  dvivthlem1  26237  dvivth  26239  pserdv  26662  logtayl  26895  goeqi  32740  reuxfrdf  32952  psrmonmul  34047  sxbrsigalem0  34769  bnj852  35417  bnj1145  35489  tz9.1regs  35647  cvmsss2  35840  cvmliftphtlem  35883  dfon2lem1  36347  dfon2lem3  36349  dfon2lem7  36353  disjeq12i  36800  ptrest  38355  mblfinlem2  38394  voliunnfl  38400  sdclem2  38479  dmmzp  43565  arearect  44043  areaquad  44044  trclrelexplem  44538  corcltrcl  44566  cotrclrcl  44569  clsk3nimkb  44867  lhe4.4ex1a  45140  wfaxsep  45805  wfaxpow  45807  wfaxun  45809  dvcosax  46741  fourierdlem57  46978  fourierdlem58  46979  fourierdlem62  46983  nnsgrpnmnd  49080  elbigofrcl  49467  iunordi  50590