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

Theorem mpg 1340
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 1338 . 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 1241
This theorem was proved from axioms:  ax-mp 7  ax-gen 1338
This theorem is referenced by:  alimi  1344  albii  1359  a5i  1435  eximi  1491  exbii  1496  19.9h  1534  hbn  1544  chvar  1640  equsb1  1668  equsb2  1669  chvarv  1812  moimi  1965  2eumo  1988  vtoclf  2607  vtocl2  2609  vtocl3  2610  spcimgf  2633  spcimegf  2634  spcgf  2635  spcegf  2636  mosub  2719  csbexa  3886  nalset  3887  ssopab2i  4014  eusv2nf  4188  iotabii  4889  fvmptss2  5247  eufnfv  5389  riotaexg  5472  xpcomco  6300  bj-ex  9902  ch2var  9907  bj-vtoclgf  9915  elabgf1  9918  bj-rspg  9926  bdsepnf  10008  bj-nalset  10015  setindf  10091  strcollnf  10110
  Copyright terms: Public domain W3C validator