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

Theorem mpg 1381
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 1379 . 2 𝑥𝜑
3 mpg.1 . 2 (∀𝑥𝜑𝜓)
42, 3ax-mp 7 1 𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1283
This theorem was proved from axioms:  ax-mp 7  ax-gen 1379
This theorem is referenced by:  alimi  1385  albii  1400  a5i  1476  eximi  1532  exbii  1537  19.9h  1575  hbn  1585  chvar  1682  equsb1  1710  equsb2  1711  chvarv  1855  moimi  2008  2eumo  2031  vtoclf  2661  vtocl2  2663  vtocl3  2664  spcimgf  2687  spcimegf  2688  spcgf  2689  spcegf  2690  mosub  2779  csbexa  3927  nalset  3928  ssopab2i  4060  eusv2nf  4234  iotabii  4939  fvmptss2  5299  eufnfv  5441  riotaexg  5523  xpcomco  6391  bj-ex  10833  ch2var  10838  bj-vtoclgf  10846  elabgf1  10849  bj-rspg  10857  sumdc2  10869  bdsepnf  10946  bj-nalset  10953  setindf  11028  strcollnf  11047
  Copyright terms: Public domain W3C validator