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

Theorem mpg 1800
Description: Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.)
Hypotheses
Ref Expression
mpg.1 (∀𝑥𝜑𝜓)
mpg.2 𝜑
Assertion
Ref Expression
mpg 𝜓

Proof of Theorem mpg
StepHypRef Expression
1 mpg.2 . . 3 𝜑
21ax-gen 1798 . 2 𝑥𝜑
3 mpg.1 . 2 (∀𝑥𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540
This theorem was proved from axioms:  ax-mp 5  ax-gen 1798
This theorem is referenced by:  nfth  1804  nfnth  1805  alimi  1814  al2imi  1818  albii  1822  eximi  1838  exbii  1851  nfbii  1855  chvarvv  2003  sbtALT  2073  sbn1  2106  nf5i  2143  chvarfv  2234  hbn  2292  chvar  2395  equsb1  2491  equsb2  2492  nfsb4  2500  sbtr  2516  2eumo  2639  abbii  2803  vtoclfOLD  3549  spcimgf  3580  spcgf  3582  euxfr2w  3716  euxfr2  3718  noel  4330  axsepgfromrep  5297  axnulALT  5304  csbex  5311  dtrucor  5369  eusv2nf  5393  axprlem3  5423  ssopab2i  5550  iotabii  6526  opabiotafun  6970  eufnfv  7228  snnex  7742  pwnex  7743  tz9.13  9783  unir1  9805  axac2  10458  axpowndlem3  10591  uzrdgfni  13920  uvtx01vtx  28644  setinds  34739  hbng  34769  bj-axd2d  35460  bj-exalimsi  35501  bj-hbsb3  35656  bj-nfs1  35659  sbn1ALT  35726  bj-issetw  35744  bj-abf  35778  bj-vtoclf  35784  bj-snsetex  35833  ax4fromc4  37753  ax10fromc7  37754  ax6fromc10  37755  equid1  37758  sn-axprlem3  41031  setindtrs  41750  frege97  42697  frege109  42709  pm11.11  43119  sbeqal1i  43144  axc5c4c711toc7  43149  axc5c4c711to11  43150  iotaequ  43174  mof0  47458  setrec2lem2  47693  vsetrec  47702
  Copyright terms: Public domain W3C validator