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

Theorem mpg 1558
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 1556 . 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 1550
This theorem is referenced by:  alimi  1569  albii  1576  eximi  1586  exbii  1593  spfw  1704  spwOLD  1708  19.9hOLD  1796  hbn  1802  chvar  1969  chvarvOLD  1971  cbv3hOLD  1978  cbv3OLD  1979  sbt  2093  equsb1  2103  equsb2  2104  nfsb4  2131  ax5  2225  ax6  2226  ax9from9o  2227  equid1  2237  moimi  2330  2eumo  2356  vtoclf  3007  vtocl2  3009  vtocl3  3010  spcimgf  3031  spcgf  3033  euxfr2  3121  csbex  3264  axsep  4331  axnulALT  4338  dtrucor  4399  ssopab2i  4484  eusv2nf  4723  iotabii  5442  eufnfv  5974  opabiotafun  6538  tz9.13  7719  unir1  7741  axac2  8348  axpowndlem3  8476  uzrdgfni  11300  setinds  25407  hbng  25438  setindtrs  27098  pm11.11  27549  sbeqal1i  27577  ax4567to6  27583  ax4567to7  27584  iotaequ  27608  cbv3wAUX7  29579  equsb1NEW7  29600  equsb2NEW7  29601  nfsb4wAUX7  29639  chvarNEW7  29682  chvarvNEW7  29688  cbv3OLD7  29785  cbv3hOLD7  29786  nfsb4OLD7  29809
This theorem was proved from axioms:  ax-mp 8  ax-gen 1556
  Copyright terms: Public domain W3C validator