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

Theorem mpg 1794
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 1792 . 2 𝑥𝜑
3 mpg.1 . 2 (∀𝑥𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1531
This theorem was proved from axioms:  ax-mp 5  ax-gen 1792
This theorem is referenced by:  nfth  1798  nfnth  1799  alimi  1808  al2imi  1812  albii  1816  eximi  1831  exbii  1844  nfbii  1848  chvarvv  2001  sbtALT  2070  equsb1vOLD  2109  nf5i  2146  chvarfv  2238  hbn  2299  chvar  2409  equsb1  2526  equsb2  2527  nfsb4  2536  sbtr  2554  equsb1ALT  2597  nfsb4ALT  2601  moimiOLD  2624  mobiiOLD  2628  eubiiOLD  2667  2eumo  2723  abbii  2886  vtoclf  3558  vtocl  3559  vtocl2OLD  3562  spcimgf  3587  spcgf  3589  euxfr2w  3710  euxfr2  3712  axsepgfromrep  5200  axnulALT  5207  csbex  5214  dtrucor  5271  eusv2nf  5295  axprlem3  5325  ssopab2i  5436  iotabii  6339  opabiotafun  6743  eufnfv  6990  snnex  7479  pwnex  7480  tz9.13  9219  unir1  9241  axac2  9887  axpowndlem3  10020  uzrdgfni  13325  uvtx01vtx  27178  setinds  33023  hbng  33053  bj-axd2d  33927  bj-exalimsi  33968  bj-hbsb3  34111  bj-nfs1  34114  bj-issetw  34190  bj-abf  34225  bj-vtoclf  34231  bj-snsetex  34275  ax4fromc4  36029  ax10fromc7  36030  ax6fromc10  36031  equid1  36034  sn-axprlem3  39109  setindtrs  39622  frege97  40306  frege109  40318  pm11.11  40706  sbeqal1i  40731  axc5c4c711toc7  40736  axc5c4c711to11  40737  iotaequ  40761  setrec2lem2  44798  vsetrec  44806
  Copyright terms: Public domain W3C validator