Theorem mpg 1681

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

Step	Hyp	Ref	Expression
1		mpg.2	. . 3 |- ph
2	1	ax-gen 1679	. 2 |- A. x ph
3		mpg.1	. 2 |- ( A. x ph -> ps )
4	2, 3	ax-mp 5	1 |- ps

Syntax hints:   -> wi 4   A.wal 1452

This theorem was proved from axioms:  ax-mp 5  ax-gen 1679

This theorem is referenced by:  alimi  1694  al2imi  1697  albii  1701  eximi  1717  exbii  1728  spfw  1885  hbn  1987  chvar  2116  equsb1  2207  equsb2  2208  nfsb4  2229  sbt  2258  sbtr  2260  moimi  2359  2eumo  2384  vtoclf  3110  vtocl  3111  vtocl2  3113  vtocl3  3114  spcimgf  3138  spcgf  3140  euxfr2  3234  axsep  4537  axnulALT  4544  csbex  4551  eusv2nf  4614  dtrucor  4646  ssopab2i  4742  iotabii  5586  opabiotafun  5948  eufnfv  6163  tz9.13  8287  unir1  8309  axac2  8921  axpowndlem3  9049  uzrdgfni  12203  setinds  30472  hbng  30503  bj-axd2d  31220  bj-nfth  31242  bj-nfnth  31244  bj-nfxfr  31262  bj-ssbimi  31280  bj-ssbbii  31281  bj-hbsb3  31358  bj-nfs1  31361  bj-chvarv  31370  bj-chvarvv  31371  bj-equsb1v  31419  bj-sbtv  31422  bj-axsep  31452  bj-dtrucor  31459  bj-vexw  31508  bj-vexwv  31510  bj-issetw  31513  bj-abf  31554  bj-vtoclf  31559  bj-snsetex  31601  ax4  32510  ax10  32511  ax6fromc10  32512  equid1  32522  setindtrs  35924  frege97  36600  frege109  36612  pm11.11  36766  sbeqal1i  36792  axc5c4c711toc7  36798  axc5c4c711to11  36799  iotaequ  36823  uvtxa01vtx0  39518