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

Theorem mprg 3149
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 3145 . 2 𝑥𝐴 𝜑
3 mprg.1 . 2 (∀𝑥𝐴 𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  wral 3135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787
This theorem depends on definitions:  df-bi 208  df-ral 3140
This theorem is referenced by:  reximia  3239  rmoimia  3729  reuxfrd  3736  2reurmo  3748  iuneq2i  4931  iineq2i  4932  dfiun2  4949  dfiin2  4950  eusv4  5297  dfiun3  5830  dfiin3  5831  relmptopab  7384  fsplitfpar  7803  ixpint  8477  noinfep  9111  tctr  9170  r1elssi  9222  ackbij2  9653  hsmexlem5  9840  axcc2lem  9846  inar1  10185  ccatalpha  13935  sumeq2i  15044  sum2id  15053  prodeq2i  15261  prod2id  15270  prdsbasex  16712  fnmrc  16866  sscpwex  17073  gsumwspan  17999  0frgp  18834  subdrgint  19511  psrbaglefi  20080  mvrf1  20133  mplmonmul  20173  frgpcyg  20648  elpt  22108  ptbasin2  22114  ptbasfi  22117  ptcld  22149  ptrescn  22175  xkoinjcn  22223  ptuncnv  22343  ptunhmeo  22344  itgfsum  24354  rolle  24514  dvlip  24517  dvivthlem1  24532  dvivth  24534  pserdv  24944  logtayl  25170  goeqi  29977  reuxfrdf  30182  sxbrsigalem0  31428  bnj852  32092  bnj1145  32162  cvmsss2  32418  cvmliftphtlem  32461  dfon2lem1  32925  dfon2lem3  32927  dfon2lem7  32931  ptrest  34772  mblfinlem2  34811  voliunnfl  34817  sdclem2  34898  dmmzp  39208  arearect  39700  areaquad  39701  trclrelexplem  39934  corcltrcl  39962  cotrclrcl  39965  clsk3nimkb  40268  lhe4.4ex1a  40538  dvcosax  42087  fourierdlem57  42325  fourierdlem58  42326  fourierdlem62  42330  nnsgrpnmnd  43962  elbigofrcl  44538  iunordi  44708
  Copyright terms: Public domain W3C validator