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

Theorem mpg 1438
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 1436 . 2 𝑥𝜑
3 mpg.1 . 2 (∀𝑥𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1340
This theorem was proved from axioms:  ax-mp 5  ax-gen 1436
This theorem is referenced by:  alimi  1442  albii  1457  a5i  1530  nfal  1563  eximi  1587  exbii  1592  19.9h  1630  hbn  1641  chvarfv  1687  chvar  1744  equsb1  1772  equsb2  1773  chvarvv  1895  chvarv  1924  moimi  2078  2eumo  2101  vtoclf  2777  vtocl2  2779  vtocl3  2780  spcimgf  2804  spcimegf  2805  spcgf  2806  spcegf  2807  mosub  2902  csbexa  4108  nalset  4109  ssopab2i  4252  pwnex  4424  eusv2nf  4431  iotabii  5172  fvmptss2  5558  eufnfv  5712  riotaexg  5799  xpcomco  6786  bj-ex  13536  ch2var  13541  bj-vtoclgf  13550  elabgf1  13553  bj-rspg  13561  sumdc2  13573  bdsepnf  13663  bj-nalset  13670  setindf  13741  strcollnf  13760
  Copyright terms: Public domain W3C validator