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

Theorem mprg 3073
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 3069 . 2 𝑥𝐴 𝜑
3 mprg.1 . 2 (∀𝑥𝐴 𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2155  wral 3055
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890
This theorem depends on definitions:  df-bi 198  df-ral 3060
This theorem is referenced by:  reximia  3155  rmoimia  3569  iuneq2i  4695  iineq2i  4696  dfiun2  4710  dfiin2  4711  eusv4  5041  reuxfr2d  5054  dfiun3  5549  dfiin3  5550  relmptopab  7081  ixpint  8140  noinfep  8772  tctr  8831  r1elssi  8883  ackbij2  9318  hsmexlem5  9505  axcc2lem  9511  inar1  9850  ccatalpha  13564  sumeq2i  14716  sum2id  14726  prodeq2i  14934  prod2id  14943  prdsbasex  16379  fnmrc  16535  sscpwex  16742  gsumwspan  17652  0frgp  18458  psrbaglefi  19646  mvrf1  19699  mplmonmul  19738  frgpcyg  20194  elpt  21655  ptbasin2  21661  ptbasfi  21664  ptcld  21696  ptrescn  21722  xkoinjcn  21770  ptuncnv  21890  ptunhmeo  21891  itgfsum  23884  rolle  24044  dvlip  24047  dvivthlem1  24062  dvivth  24064  pserdv  24474  logtayl  24697  goeqi  29523  reuxfr3d  29718  sxbrsigalem0  30715  bnj852  31371  bnj1145  31441  cvmsss2  31636  cvmliftphtlem  31679  dfon2lem1  32063  dfon2lem3  32065  dfon2lem7  32069  ptrest  33764  mblfinlem2  33803  voliunnfl  33809  sdclem2  33892  dmmzp  37906  arearect  38409  areaquad  38410  trclrelexplem  38610  corcltrcl  38638  cotrclrcl  38641  clsk3nimkb  38944  lhe4.4ex1a  39134  dvcosax  40711  fourierdlem57  40949  fourierdlem58  40950  fourierdlem62  40954  2reurmo  41785  nnsgrpnmnd  42419  elbigofrcl  42945  iunordi  43024
  Copyright terms: Public domain W3C validator