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

Theorem mpg 1538
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 1536 . 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 1530
This theorem is referenced by:  alimi  1549  albii  1556  eximi  1566  exbii  1572  spfw  1676  spw  1679  19.9h  1739  cbv3  1935  cbv3h  1936  chvar  1939  chvarv  1966  equsb1  1987  equsb2  1988  nfsb4  2034  ax5  2098  ax6  2099  ax9from9o  2100  equid1  2110  moimi  2203  2eumo  2229  vtoclf  2850  vtocl2  2852  vtocl3  2853  spcimgf  2874  spcgf  2876  euxfr2  2963  csbex  3105  axsep  4156  axnulALT  4163  dtrucor  4224  ssopab2i  4308  eusv2nf  4548  iotabii  5257  eufnfv  5768  opabiotafun  6307  tz9.13  7479  unir1  7501  axac3OLD  8107  axac2  8109  axpowndlem3  8237  uzrdgfni  11037  setinds  24205  hbng  24236  setindtrs  27221  pm11.11  27673  sbeqal1i  27701  ax4567to6  27707  ax4567to7  27708  iotaequ  27732  cbv3wAUX7  29492  cbv3hwAUX7  29493  equsb1NEW7  29513  equsb2NEW7  29514  nfsb4wAUX7  29552  chvarNEW7  29592  chvarvNEW7  29598  cbv3OLD7  29677  cbv3hOLD7  29678  nfsb4OLD7  29701
This theorem was proved from axioms:  ax-mp 8  ax-gen 1536
  Copyright terms: Public domain W3C validator