ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpg 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  9237  ch2var  9242  bj-vtoclgf  9250  elabgf1  9253  bj-rspg  9261  bdsepnf  9343  bj-nalset  9350  setindf  9426  strcollnf  9445
  Copyright terms: Public domain W3C validator