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

Theorem mpg 1316
Description: Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.)
Hypotheses
Ref Expression
mpg.1 (xφψ)
mpg.2 φ
Assertion
Ref Expression
mpg ψ

Proof of Theorem mpg
StepHypRef Expression
1 mpg.2 . . 3 φ
21ax-gen 1314 . 2 xφ
3 mpg.1 . 2 (xφψ)
42, 3ax-mp 7 1 ψ
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1224
This theorem was proved from axioms:  ax-mp 7  ax-gen 1314
This theorem is referenced by:  alimi  1320  albii  1335  a5i  1413  eximi  1469  exbii  1474  19.9h  1512  hbn  1522  chvar  1618  equsb1  1646  equsb2  1647  chvarv  1790  moimi  1943  2eumo  1966  vtoclf  2580  vtocl2  2582  vtocl3  2583  spcimgf  2606  spcimegf  2607  spcgf  2608  spcegf  2609  mosub  2692  csbexOLD  3856  nalset  3857  ssopab2i  3984  eusv2nf  4134  iotabii  4812  fvmptss2  5168  eufnfv  5310  bj-ex  7201  ch2var  7206  bj-vtoclgf  7214  elabgf1  7217  bj-rspg  7225  bdsepnf  7306  bj-nalset  7310  setindf  7380  strcollnf  7399
  Copyright terms: Public domain W3C validator