Theorem mprg 3068

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

Syntax hints:   → wi 4   ∈ wcel 2107  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  reximiaOLD  3089  rmoimia  3738  reuxfrd  3745  2reurmo  3756  ralf0  4514  iuneq2i  5019  iineq2i  5020  dfiun2  5037  dfiin2  5038  eusv4  5405  dfiun3  5966  dfiin3  5967  relmptopab  7656  fsplitfpar  8104  ixpint  8919  noinfep  9655  tctr  9735  r1elssi  9800  ackbij2  10238  hsmexlem5  10425  axcc2lem  10431  inar1  10770  ccatalpha  14543  sumeq2i  15645  sum2id  15654  prodeq2i  15863  prod2id  15872  prdsbasex  17396  fnmrc  17551  sscpwex  17762  gsumwspan  18727  0frgp  19647  subdrgint  20419  frgpcyg  21129  psrbaglefi  21485  psrbaglefiOLD  21486  mvrf1  21545  mplmonmul  21591  elpt  23076  ptbasin2  23082  ptbasfi  23085  ptcld  23117  ptrescn  23143  xkoinjcn  23191  ptuncnv  23311  ptunhmeo  23312  itgfsum  25344  rolle  25507  dvlip  25510  dvivthlem1  25525  dvivth  25527  pserdv  25941  logtayl  26168  goeqi  31526  reuxfrdf  31731  sxbrsigalem0  33270  bnj852  33932  bnj1145  34004  cvmsss2  34265  cvmliftphtlem  34308  dfon2lem1  34755  dfon2lem3  34757  dfon2lem7  34761  ptrest  36487  mblfinlem2  36526  voliunnfl  36532  sdclem2  36610  dmmzp  41471  arearect  41964  areaquad  41965  trclrelexplem  42462  corcltrcl  42490  cotrclrcl  42493  clsk3nimkb  42791  lhe4.4ex1a  43088  dvcosax  44642  fourierdlem57  44879  fourierdlem58  44880  fourierdlem62  44884  nnsgrpnmnd  46588  elbigofrcl  47236  iunordi  47722