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

Theorem mpg 1356
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 1354 . 2 𝑥𝜑
3 mpg.1 . 2 (∀𝑥𝜑𝜓)
42, 3ax-mp 7 1 𝜓
Colors of variables: wff set class
Syntax hints:  wi 4  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  2741  csbexa  3913  nalset  3914  ssopab2i  4041  eusv2nf  4215  iotabii  4916  fvmptss2  5274  eufnfv  5416  riotaexg  5499  xpcomco  6330  bj-ex  10261  ch2var  10266  bj-vtoclgf  10274  elabgf1  10277  bj-rspg  10285  bdsepnf  10367  bj-nalset  10374  setindf  10450  strcollnf  10469
  Copyright terms: Public domain W3C validator