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

Theorem mpg 1383
Description: Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.)
Hypotheses
Ref Expression
mpg.1  |-  ( A. x ph  ->  ps )
mpg.2  |-  ph
Assertion
Ref Expression
mpg  |-  ps

Proof of Theorem mpg
StepHypRef Expression
1 mpg.2 . . 3  |-  ph
21ax-gen 1381 . 2  |-  A. x ph
3 mpg.1 . 2  |-  ( A. x ph  ->  ps )
42, 3ax-mp 7 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1285
This theorem was proved from axioms:  ax-mp 7  ax-gen 1381
This theorem is referenced by:  alimi  1387  albii  1402  a5i  1478  eximi  1534  exbii  1539  19.9h  1577  hbn  1587  chvar  1684  equsb1  1712  equsb2  1713  chvarv  1857  moimi  2010  2eumo  2033  vtoclf  2666  vtocl2  2668  vtocl3  2669  spcimgf  2692  spcimegf  2693  spcgf  2694  spcegf  2695  mosub  2784  csbexa  3942  nalset  3943  ssopab2i  4077  eusv2nf  4251  iotabii  4965  fvmptss2  5336  eufnfv  5480  riotaexg  5567  xpcomco  6488  bj-ex  11093  ch2var  11098  bj-vtoclgf  11106  elabgf1  11109  bj-rspg  11117  sumdc2  11129  bdsepnf  11209  bj-nalset  11216  setindf  11291  strcollnf  11310
  Copyright terms: Public domain W3C validator