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

Theorem mpg 1385
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 1383 . 2 𝑥𝜑
3 mpg.1 . 2 (∀𝑥𝜑𝜓)
42, 3ax-mp 7 1 𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1287
This theorem was proved from axioms:  ax-mp 7  ax-gen 1383
This theorem is referenced by:  alimi  1389  albii  1404  a5i  1480  eximi  1536  exbii  1541  19.9h  1579  hbn  1589  chvar  1687  equsb1  1715  equsb2  1716  chvarv  1860  moimi  2013  2eumo  2036  vtoclf  2672  vtocl2  2674  vtocl3  2675  spcimgf  2699  spcimegf  2700  spcgf  2701  spcegf  2702  mosub  2791  csbexa  3960  nalset  3961  ssopab2i  4095  eusv2nf  4269  iotabii  4989  fvmptss2  5363  eufnfv  5507  riotaexg  5594  xpcomco  6522  bj-ex  11309  ch2var  11314  bj-vtoclgf  11322  elabgf1  11325  bj-rspg  11333  sumdc2  11345  bdsepnf  11425  bj-nalset  11432  setindf  11507  strcollnf  11526
  Copyright terms: Public domain W3C validator