Theorem mprg 3051

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

Syntax hints:   → wi 4   ∈ wcel 2109  ∀wral 3045

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

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

This theorem is referenced by:  rmoimia  3715  reuxfrd  3722  2reurmo  3733  rabxm  4356  ralf0  4480  iuneq2i  4980  iineq2i  4981  dfiun2  5000  dfiin2  5001  eusv4  5364  dfiun3  5936  dfiin3  5937  relmptopab  7642  fsplitfpar  8100  ixpint  8901  noinfep  9620  tctr  9700  r1elssi  9765  ackbij2  10202  hsmexlem5  10390  axcc2lem  10396  inar1  10735  ccatalpha  14565  sumeq2i  15671  sum2id  15681  prodeq2i  15891  prod2id  15901  prdsbasex  17420  fnmrc  17575  sscpwex  17784  gsumwspan  18780  0frgp  19716  subdrgint  20719  frgpcyg  21490  psrbaglefi  21842  mvrf1  21902  mplmonmul  21950  elpt  23466  ptbasin2  23472  ptbasfi  23475  ptcld  23507  ptrescn  23533  xkoinjcn  23581  ptuncnv  23701  ptunhmeo  23702  itgfsum  25735  rolle  25901  dvlip  25905  dvivthlem1  25920  dvivth  25922  pserdv  26346  logtayl  26576  goeqi  32209  reuxfrdf  32427  sxbrsigalem0  34269  bnj852  34918  bnj1145  34990  cvmsss2  35268  cvmliftphtlem  35311  dfon2lem1  35778  dfon2lem3  35780  dfon2lem7  35784  disjeq12i  36188  ptrest  37620  mblfinlem2  37659  voliunnfl  37665  sdclem2  37743  dmmzp  42728  arearect  43211  areaquad  43212  trclrelexplem  43707  corcltrcl  43735  cotrclrcl  43738  clsk3nimkb  44036  lhe4.4ex1a  44325  wfaxsep  44992  wfaxpow  44994  wfaxun  44996  dvcosax  45931  fourierdlem57  46168  fourierdlem58  46169  fourierdlem62  46173  nnsgrpnmnd  48170  elbigofrcl  48543  iunordi  49670