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

Theorem mpg 1535
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 1533 . 2  |-  A. x ph
3 mpg.1 . 2  |-  ( A. x ph  ->  ps )
42, 3ax-mp 8 1  |-  ps
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527
This theorem is referenced by:  alimi  1546  albii  1553  eximi  1563  exbii  1569  spfw  1657  spw  1660  19.9h  1727  cbv3  1922  cbv3h  1923  chvar  1926  chvarv  1953  equsb1  1974  equsb2  1975  nfsb4  2021  ax5  2085  ax6  2086  ax9from9o  2087  equid1  2097  moimi  2190  2eumo  2216  vtoclf  2837  vtocl2  2839  vtocl3  2840  spcimgf  2861  spcgf  2863  euxfr2  2950  csbex  3092  axsep  4140  axnulALT  4147  dtrucor  4208  ssopab2i  4292  eusv2nf  4532  iotabii  5241  eufnfv  5752  opabiotafun  6291  tz9.13  7463  unir1  7485  axac3OLD  8091  axac2  8093  axpowndlem3  8221  uzrdgfni  11021  setinds  24134  hbng  24165  setindtrs  27118  pm11.11  27570  sbeqal1i  27598  ax4567to6  27604  ax4567to7  27605  iotaequ  27629
This theorem was proved from axioms:  ax-mp 8  ax-gen 1533
  Copyright terms: Public domain W3C validator