ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpg GIF version

Theorem mpg 1462
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 1460 . 2 𝑥𝜑
3 mpg.1 . 2 (∀𝑥𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1362
This theorem was proved from axioms:  ax-mp 5  ax-gen 1460
This theorem is referenced by:  alimi  1466  albii  1481  a5i  1554  nfal  1587  eximi  1611  exbii  1616  19.9h  1654  hbn  1665  chvarfv  1711  chvar  1768  equsb1  1796  equsb2  1797  chvarvv  1920  chvarv  1949  moimi  2103  2eumo  2126  vtoclf  2805  vtocl2  2807  vtocl3  2808  spcimgf  2832  spcimegf  2833  spcgf  2834  spcegf  2835  mosub  2930  csbexa  4147  nalset  4148  ssopab2i  4295  pwnex  4467  eusv2nf  4474  iotabii  5219  fvmptss2  5611  eufnfv  5767  riotaexg  5855  xpcomco  6851  bj-ex  14967  ch2var  14972  bj-vtoclgf  14981  elabgf1  14984  bj-rspg  14992  sumdc2  15004  bdsepnf  15093  bj-nalset  15100  setindf  15171  strcollnf  15190
  Copyright terms: Public domain W3C validator