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

Theorem mprg 3156
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 3152 . 2 𝑥𝐴 𝜑
3 mprg.1 . 2 (∀𝑥𝐴 𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wral 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789
This theorem depends on definitions:  df-bi 208  df-ral 3147
This theorem is referenced by:  reximia  3246  rmoimia  3735  reuxfrd  3742  2reurmo  3754  iuneq2i  4936  iineq2i  4937  dfiun2  4954  dfiin2  4955  eusv4  5302  dfiun3  5835  dfiin3  5836  relmptopab  7388  fsplitfpar  7808  ixpint  8481  noinfep  9115  tctr  9174  r1elssi  9226  ackbij2  9657  hsmexlem5  9844  axcc2lem  9850  inar1  10189  ccatalpha  13940  sumeq2i  15049  sum2id  15058  prodeq2i  15266  prod2id  15275  prdsbasex  16717  fnmrc  16871  sscpwex  17078  gsumwspan  17997  0frgp  18828  subdrgint  19505  psrbaglefi  20074  mvrf1  20127  mplmonmul  20166  frgpcyg  20639  elpt  22099  ptbasin2  22105  ptbasfi  22108  ptcld  22140  ptrescn  22166  xkoinjcn  22214  ptuncnv  22334  ptunhmeo  22335  itgfsum  24345  rolle  24505  dvlip  24508  dvivthlem1  24523  dvivth  24525  pserdv  24935  logtayl  25159  goeqi  29967  reuxfrdf  30172  sxbrsigalem0  31418  bnj852  32082  bnj1145  32152  cvmsss2  32408  cvmliftphtlem  32451  dfon2lem1  32915  dfon2lem3  32917  dfon2lem7  32921  ptrest  34761  mblfinlem2  34800  voliunnfl  34806  sdclem2  34888  dmmzp  39198  arearect  39690  areaquad  39691  trclrelexplem  39924  corcltrcl  39952  cotrclrcl  39955  clsk3nimkb  40258  lhe4.4ex1a  40529  dvcosax  42079  fourierdlem57  42317  fourierdlem58  42318  fourierdlem62  42322  nnsgrpnmnd  43920  elbigofrcl  44445  iunordi  44615
  Copyright terms: Public domain W3C validator