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

Theorem mpg 1337
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 1335 . 2
3 mpg.1 . 2
42, 3ax-mp 7 1
Colors of variables: wff set class
Syntax hints:   wi 4  wal 1240
This theorem was proved from axioms:  ax-mp 7  ax-gen 1335
This theorem is referenced by:  alimi  1341  albii  1356  a5i  1432  eximi  1488  exbii  1493  19.9h  1531  hbn  1541  chvar  1637  equsb1  1665  equsb2  1666  chvarv  1809  moimi  1962  2eumo  1985  vtoclf  2601  vtocl2  2603  vtocl3  2604  spcimgf  2627  spcimegf  2628  spcgf  2629  spcegf  2630  mosub  2713  csbexa  3877  nalset  3878  ssopab2i  4005  eusv2nf  4154  iotabii  4832  fvmptss2  5190  eufnfv  5332  riotaexg  5415  xpcomco  6236  bj-ex  9217  ch2var  9222  bj-vtoclgf  9230  elabgf1  9233  bj-rspg  9241  bdsepnf  9322  bj-nalset  9326  setindf  9396  strcollnf  9415
  Copyright terms: Public domain W3C validator