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

Theorem mprg 3057
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 3053 . 2 𝑥𝐴 𝜑
3 mprg.1 . 2 (∀𝑥𝐴 𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2098  wral 3051
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 206  df-ral 3052
This theorem is referenced by:  reximiaOLD  3078  rmoimia  3734  reuxfrd  3741  2reurmo  3752  rabxm  4387  ralf0  4514  iuneq2i  5017  iineq2i  5018  dfiun2  5036  dfiin2  5037  eusv4  5405  dfiun3  5968  dfiin3  5969  relmptopab  7669  fsplitfpar  8121  ixpint  8942  noinfep  9683  tctr  9763  r1elssi  9828  ackbij2  10266  hsmexlem5  10453  axcc2lem  10459  inar1  10798  ccatalpha  14575  sumeq2i  15677  sum2id  15686  prodeq2i  15895  prod2id  15904  prdsbasex  17431  fnmrc  17586  sscpwex  17797  gsumwspan  18802  0frgp  19738  subdrgint  20695  frgpcyg  21511  psrbaglefi  21869  psrbaglefiOLD  21870  mvrf1  21935  mplmonmul  21981  elpt  23506  ptbasin2  23512  ptbasfi  23515  ptcld  23547  ptrescn  23573  xkoinjcn  23621  ptuncnv  23741  ptunhmeo  23742  itgfsum  25786  rolle  25952  dvlip  25956  dvivthlem1  25971  dvivth  25973  pserdv  26396  logtayl  26624  goeqi  32139  reuxfrdf  32346  sxbrsigalem0  33961  bnj852  34622  bnj1145  34694  cvmsss2  34954  cvmliftphtlem  34997  dfon2lem1  35449  dfon2lem3  35451  dfon2lem7  35455  ptrest  37162  mblfinlem2  37201  voliunnfl  37207  sdclem2  37285  dmmzp  42218  arearect  42708  areaquad  42709  trclrelexplem  43206  corcltrcl  43234  cotrclrcl  43237  clsk3nimkb  43535  lhe4.4ex1a  43831  dvcosax  45377  fourierdlem57  45614  fourierdlem58  45615  fourierdlem62  45619  nnsgrpnmnd  47352  elbigofrcl  47735  iunordi  48220
  Copyright terms: Public domain W3C validator