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

Theorem mpg 1427
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 1425 . 2 𝑥𝜑
3 mpg.1 . 2 (∀𝑥𝜑𝜓)
42, 3ax-mp 5 1 𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1329
This theorem was proved from axioms:  ax-mp 5  ax-gen 1425
This theorem is referenced by:  alimi  1431  albii  1446  a5i  1522  eximi  1579  exbii  1584  19.9h  1622  hbn  1632  chvar  1730  equsb1  1758  equsb2  1759  chvarvv  1880  chvarv  1907  moimi  2062  2eumo  2085  vtoclf  2734  vtocl2  2736  vtocl3  2737  spcimgf  2761  spcimegf  2762  spcgf  2763  spcegf  2764  mosub  2857  csbexa  4052  nalset  4053  ssopab2i  4194  pwnex  4365  eusv2nf  4372  iotabii  5105  fvmptss2  5489  eufnfv  5641  riotaexg  5727  xpcomco  6713  bj-ex  12958  ch2var  12963  bj-vtoclgf  12972  elabgf1  12975  bj-rspg  12983  sumdc2  12995  bdsepnf  13075  bj-nalset  13082  setindf  13153  strcollnf  13172
  Copyright terms: Public domain W3C validator