Theorem mprg 3120

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

Syntax hints:   → wi 4   ∈ wcel 2111  ∀wral 3106

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

This theorem depends on definitions:  df-bi 210  df-ral 3111

This theorem is referenced by:  reximia  3205  rmoimia  3680  reuxfrd  3687  2reurmo  3699  iuneq2i  4902  iineq2i  4903  dfiun2  4920  dfiin2  4921  eusv4  5272  dfiun3  5802  dfiin3  5803  relmptopab  7375  fsplitfpar  7797  ixpint  8472  noinfep  9107  tctr  9166  r1elssi  9218  ackbij2  9654  hsmexlem5  9841  axcc2lem  9847  inar1  10186  ccatalpha  13938  sumeq2i  15048  sum2id  15057  prodeq2i  15265  prod2id  15274  prdsbasex  16716  fnmrc  16870  sscpwex  17077  gsumwspan  18003  0frgp  18897  subdrgint  19575  frgpcyg  20265  psrbaglefi  20610  mvrf1  20663  mplmonmul  20704  elpt  22177  ptbasin2  22183  ptbasfi  22186  ptcld  22218  ptrescn  22244  xkoinjcn  22292  ptuncnv  22412  ptunhmeo  22413  itgfsum  24430  rolle  24593  dvlip  24596  dvivthlem1  24611  dvivth  24613  pserdv  25024  logtayl  25251  goeqi  30056  reuxfrdf  30262  sxbrsigalem0  31639  bnj852  32303  bnj1145  32375  cvmsss2  32634  cvmliftphtlem  32677  dfon2lem1  33141  dfon2lem3  33143  dfon2lem7  33147  ptrest  35056  mblfinlem2  35095  voliunnfl  35101  sdclem2  35180  dmmzp  39674  arearect  40165  areaquad  40166  trclrelexplem  40412  corcltrcl  40440  cotrclrcl  40443  clsk3nimkb  40743  lhe4.4ex1a  41033  dvcosax  42568  fourierdlem57  42805  fourierdlem58  42806  fourierdlem62  42810  nnsgrpnmnd  44438  elbigofrcl  44964  iunordi  45207