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

Theorem mprg 3075
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 3071 . 2 𝑥𝐴 𝜑
3 mprg.1 . 2 (∀𝑥𝐴 𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  wral 3061
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870
This theorem depends on definitions:  df-bi 197  df-ral 3066
This theorem is referenced by:  reximia  3157  rmoimia  3560  iuneq2i  4673  iineq2i  4674  dfiun2  4688  dfiin2  4689  eusv4  5006  reuxfr2d  5019  dfiun3  5518  dfiin3  5519  relmptopab  7030  ixpint  8089  noinfep  8721  tctr  8780  r1elssi  8832  ackbij2  9267  hsmexlem5  9454  axcc2lem  9460  inar1  9799  ccatalpha  13575  sumeq2i  14637  sum2id  14647  prodeq2i  14856  prod2id  14865  prdsbasex  16319  fnmrc  16475  sscpwex  16682  gsumwspan  17591  0frgp  18399  psrbaglefi  19587  mvrf1  19640  mplmonmul  19679  frgpcyg  20137  elpt  21596  ptbasin2  21602  ptbasfi  21605  ptcld  21637  ptrescn  21663  xkoinjcn  21711  ptuncnv  21831  ptunhmeo  21832  itgfsum  23813  rolle  23973  dvlip  23976  dvivthlem1  23991  dvivth  23993  pserdv  24403  logtayl  24627  goeqi  29472  reuxfr3d  29668  sxbrsigalem0  30673  bnj852  31329  bnj1145  31399  cvmsss2  31594  cvmliftphtlem  31637  dfon2lem1  32024  dfon2lem3  32026  dfon2lem7  32030  ptrest  33741  mblfinlem2  33780  voliunnfl  33786  sdclem2  33870  dmmzp  37822  arearect  38327  areaquad  38328  trclrelexplem  38529  corcltrcl  38557  cotrclrcl  38560  clsk3nimkb  38864  lhe4.4ex1a  39054  dvcosax  40659  fourierdlem57  40897  fourierdlem58  40898  fourierdlem62  40902  2reurmo  41702  nnsgrpnmnd  42346  elbigofrcl  42872  iunordi  42951
  Copyright terms: Public domain W3C validator