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

Theorem mpg 1668
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 1666 . 2  |-  A. x ph
3 mpg.1 . 2  |-  ( A. x ph  ->  ps )
42, 3ax-mp 5 1  |-  ps
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1436
This theorem was proved from axioms:  ax-mp 5  ax-gen 1666
This theorem is referenced by:  alimi  1681  al2imi  1684  albii  1688  eximi  1703  exbii  1713  spfw  1857  hbn  1951  chvar  2068  equsb1  2161  equsb2  2162  nfsb4  2185  sbt  2214  sbtr  2216  moimi  2317  2eumo  2342  vtoclf  3133  vtocl2  3135  vtocl3  3136  spcimgf  3160  spcgf  3162  euxfr2  3257  axsep  4543  axnulALT  4550  csbex  4557  eusv2nf  4620  dtrucor  4652  ssopab2i  4746  iotabii  5585  opabiotafun  5940  eufnfv  6152  tz9.13  8265  unir1  8287  axac2  8898  axpowndlem3  9026  uzrdgfni  12173  setinds  30425  hbng  30456  bj-axd2d  31174  bj-nffal  31194  bj-nfxfr  31211  bj-hbsb3  31267  bj-nfs1  31270  bj-chvarv  31280  bj-equsb1v  31336  bj-sbtv  31340  bj-axsep  31372  bj-dtrucor  31379  bj-vexw  31428  bj-vexwv  31430  bj-issetw  31433  bj-abf  31473  bj-vtoclf  31478  bj-snsetex  31519  ax4  32429  ax10  32430  ax6fromc10  32431  equid1  32441  setindtrs  35844  frege97  36458  frege109  36470  pm11.11  36625  sbeqal1i  36651  axc5c4c711toc7  36657  axc5c4c711to11  36658  iotaequ  36682
  Copyright terms: Public domain W3C validator