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

Theorem mpg 1805
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 1803 . 2 𝑥𝜑
3 mpg.1 . 2 (∀𝑥𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1541
This theorem was proved from axioms:  ax-mp 5  ax-gen 1803
This theorem is referenced by:  nfth  1809  nfnth  1810  alimi  1819  al2imi  1823  albii  1827  eximi  1842  exbii  1855  nfbii  1859  chvarvv  2007  sbtALT  2075  sbn1  2109  nf5i  2146  chvarfv  2238  hbn  2296  chvar  2394  equsb1  2494  equsb2  2495  nfsb4  2503  sbtr  2519  2eumo  2643  abbii  2808  vtoclf  3478  spcimgf  3509  spcgf  3511  euxfr2w  3638  euxfr2  3640  noel  4250  axsepgfromrep  5195  axnulALT  5202  csbex  5209  dtrucor  5269  eusv2nf  5293  axprlem3  5323  ssopab2i  5436  iotabii  6370  opabiotafun  6797  eufnfv  7050  snnex  7548  pwnex  7549  tz9.13  9412  unir1  9434  axac2  10085  axpowndlem3  10218  uzrdgfni  13536  uvtx01vtx  27490  setinds  33478  hbng  33508  bj-axd2d  34517  bj-exalimsi  34558  bj-hbsb3  34713  bj-nfs1  34716  sbn1ALT  34784  bj-issetw  34802  bj-abf  34836  bj-vtoclf  34842  bj-snsetex  34895  ax4fromc4  36650  ax10fromc7  36651  ax6fromc10  36652  equid1  36655  sn-axprlem3  39916  setindtrs  40558  frege97  41253  frege109  41265  pm11.11  41673  sbeqal1i  41698  axc5c4c711toc7  41703  axc5c4c711to11  41704  iotaequ  41728  mof0  45846  setrec2lem2  46079  vsetrec  46087
  Copyright terms: Public domain W3C validator