MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mprg Structured version   Visualization version   GIF version

Theorem mprg 2921
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
StepHypRef Expression
1 mprg.2 . . 3 (𝑥𝐴𝜑)
21rgen 2917 . 2 𝑥𝐴 𝜑
3 mprg.1 . 2 (∀𝑥𝐴 𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  wral 2907
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719
This theorem depends on definitions:  df-bi 197  df-ral 2912
This theorem is referenced by:  reximia  3004  rmoimia  3394  iuneq2i  4510  iineq2i  4511  dfiun2  4525  dfiin2  4526  eusv4  4842  reuxfr2d  4856  dfiun3  5345  dfiin3  5346  relmptopab  6843  ixpint  7886  noinfep  8508  tctr  8567  r1elssi  8619  ackbij2  9016  hsmexlem5  9203  axcc2lem  9209  inar1  9548  ccatalpha  13321  sumeq2i  14370  sum2id  14379  prodeq2i  14581  prod2id  14590  prdsbasex  16039  fnmrc  16195  sscpwex  16403  gsumwspan  17311  0frgp  18120  psrbaglefi  19300  mvrf1  19353  mplmonmul  19392  frgpcyg  19850  elpt  21294  ptbasin2  21300  ptbasfi  21303  ptcld  21335  ptrescn  21361  xkoinjcn  21409  ptuncnv  21529  ptunhmeo  21530  itgfsum  23512  rolle  23670  dvlip  23673  dvivthlem1  23688  dvivth  23690  pserdv  24100  logtayl  24319  goeqi  28999  reuxfr3d  29196  sxbrsigalem0  30132  bnj852  30726  bnj1145  30796  cvmsss2  30991  cvmliftphtlem  31034  dfon2lem1  31416  dfon2lem3  31418  dfon2lem7  31422  ptrest  33067  mblfinlem2  33106  voliunnfl  33112  sdclem2  33197  dmmzp  36803  arearect  37309  areaquad  37310  trclrelexplem  37511  corcltrcl  37539  cotrclrcl  37542  clsk3nimkb  37847  lhe4.4ex1a  38037  dvcosax  39469  fourierdlem57  39708  fourierdlem58  39709  fourierdlem62  39713  2reurmo  40507  nnsgrpnmnd  41127  elbigofrcl  41657  iunordi  41736
  Copyright terms: Public domain W3C validator