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 5 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  4332  axnulALT  4339  dtrucor  4400  ssopab2i  4485  eusv2nf  4724  iotabii  5443  eufnfv  5975  opabiotafun  6539  tz9.13  7720  unir1  7742  axac2  8351  axpowndlem3  8479  uzrdgfni  11303  setinds  25410  hbng  25441  setindtrs  27110  pm11.11  27561  sbeqal1i  27589  ax4567to6  27595  ax4567to7  27596  iotaequ  27620  cbv3wAUX7  29591  equsb1NEW7  29612  equsb2NEW7  29613  nfsb4wAUX7  29651  chvarNEW7  29694  chvarvNEW7  29700  cbv3OLD7  29797  cbv3hOLD7  29798  nfsb4OLD7  29821
This theorem was proved from axioms:  ax-mp 5  ax-gen 1556
  Copyright terms: Public domain W3C validator