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

Theorem mpg 1356
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 1354 . 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 1257
This theorem was proved from axioms:  ax-mp 7  ax-gen 1354
This theorem is referenced by:  alimi  1360  albii  1375  a5i  1451  eximi  1507  exbii  1512  19.9h  1550  hbn  1560  chvar  1656  equsb1  1684  equsb2  1685  chvarv  1828  moimi  1981  2eumo  2004  vtoclf  2624  vtocl2  2626  vtocl3  2627  spcimgf  2650  spcimegf  2651  spcgf  2652  spcegf  2653  mosub  2742  csbexa  3914  nalset  3915  ssopab2i  4042  eusv2nf  4216  iotabii  4917  fvmptss2  5275  eufnfv  5417  riotaexg  5500  xpcomco  6331  bj-ex  10289  ch2var  10294  bj-vtoclgf  10302  elabgf1  10305  bj-rspg  10313  bdsepnf  10395  bj-nalset  10402  setindf  10478  strcollnf  10497
  Copyright terms: Public domain W3C validator