MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mpg Unicode version

Theorem mpg 1564
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 1562 . 2
3 mpg.1 . 2
42, 3ax-mp 5 1
Colors of variables: wff set class
Syntax hints:  ->wi 4  A.wal 1556
This theorem is referenced by:  alimi  1575  albii  1582  eximi  1594  exbii  1601  spfw  1710  spwOLD  1712  19.9hOLD  1794  hbn  1800  chvar  1967  chvarvOLD  1969  cbv3hOLD  1976  cbv3OLD  1977  sbt  2093  equsb1  2103  equsb2  2104  nfsb4  2131  ax4  2248  ax10  2249  ax6fromc10  2250  equid1  2260  moimi  2365  2eumo  2398  vtoclf  3055  vtocl2  3057  vtocl3  3058  spcimgf  3079  spcgf  3081  euxfr2  3170  axsep  4422  axnulALT  4429  csbex  4435  csbexOLD  4437  eusv2nf  4497  dtrucor  4532  ssopab2i  4621  iotabii  5402  opabiotafun  5745  eufnfv  5929  tz9.13  7829  unir1  7851  axac2  8460  axpowndlem3  8588  uzrdgfni  11573  setinds  26235  hbng  26266  setindtrs  28025  pm11.11  28475  sbeqal1i  28501  axc5c4c711toc7  28507  axc5c4c711to11  28508  iotaequ  28532  bj-snsetex  30670  cbv3wAUX11  30792  equsb1NEW11  30813  equsb2NEW11  30814  nfsb4wAUX11  30852  chvarNEW11  30894  chvarvNEW11  30900  cbv3OLD11  30997  cbv3hOLD11  30998  nfsb4OLD11  31021
This theorem was proved from axioms:  ax-mp 5  ax-gen 1562
  Copyright terms: Public domain W3C validator