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

Theorem mpg 1557
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 1555 . 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 1549
This theorem is referenced by:  alimi  1568  albii  1575  eximi  1585  exbii  1592  spfw  1703  spwOLD  1707  19.9hOLD  1795  hbn  1801  chvar  1968  chvarvOLD  1970  cbv3hOLD  1977  cbv3OLD  1978  equsb1  2113  equsb2  2114  nfsb4  2156  ax5  2222  ax6  2223  ax9from9o  2224  equid1  2234  moimi  2327  2eumo  2353  vtoclf  2997  vtocl2  2999  vtocl3  3000  spcimgf  3021  spcgf  3023  euxfr2  3111  csbex  3254  axsep  4321  axnulALT  4328  dtrucor  4389  ssopab2i  4474  eusv2nf  4713  iotabii  5432  eufnfv  5964  opabiotafun  6528  tz9.13  7709  unir1  7731  axac2  8338  axpowndlem3  8466  uzrdgfni  11290  setinds  25397  hbng  25428  setindtrs  27087  pm11.11  27538  sbeqal1i  27566  ax4567to6  27572  ax4567to7  27573  iotaequ  27597  cbv3wAUX7  29454  equsb1NEW7  29475  equsb2NEW7  29476  nfsb4wAUX7  29514  chvarNEW7  29557  chvarvNEW7  29563  cbv3OLD7  29660  cbv3hOLD7  29661  nfsb4OLD7  29684
This theorem was proved from axioms:  ax-mp 8  ax-gen 1555
  Copyright terms: Public domain W3C validator