Theorem mprg 3150

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

Syntax hints:   → wi 4   ∈ wcel 2108  ∀wral 3136

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

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

This theorem is referenced by:  reximia  3240  rmoimia  3730  reuxfrd  3737  2reurmo  3749  iuneq2i  4931  iineq2i  4932  dfiun2  4949  dfiin2  4950  eusv4  5297  dfiun3  5830  dfiin3  5831  relmptopab  7387  fsplitfpar  7806  ixpint  8481  noinfep  9115  tctr  9174  r1elssi  9226  ackbij2  9657  hsmexlem5  9844  axcc2lem  9850  inar1  10189  ccatalpha  13939  sumeq2i  15048  sum2id  15057  prodeq2i  15265  prod2id  15274  prdsbasex  16716  fnmrc  16870  sscpwex  17077  gsumwspan  18003  0frgp  18897  subdrgint  19574  psrbaglefi  20144  mvrf1  20197  mplmonmul  20237  frgpcyg  20712  elpt  22172  ptbasin2  22178  ptbasfi  22181  ptcld  22213  ptrescn  22239  xkoinjcn  22287  ptuncnv  22407  ptunhmeo  22408  itgfsum  24419  rolle  24579  dvlip  24582  dvivthlem1  24597  dvivth  24599  pserdv  25009  logtayl  25235  goeqi  30042  reuxfrdf  30247  sxbrsigalem0  31522  bnj852  32186  bnj1145  32258  cvmsss2  32514  cvmliftphtlem  32557  dfon2lem1  33021  dfon2lem3  33023  dfon2lem7  33027  ptrest  34883  mblfinlem2  34922  voliunnfl  34928  sdclem2  35009  dmmzp  39321  arearect  39813  areaquad  39814  trclrelexplem  40047  corcltrcl  40075  cotrclrcl  40078  clsk3nimkb  40381  lhe4.4ex1a  40652  dvcosax  42201  fourierdlem57  42439  fourierdlem58  42440  fourierdlem62  42444  nnsgrpnmnd  44076  elbigofrcl  44601  iunordi  44771