Theorem mpg 1641

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 1639	. 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 1403

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

This theorem is referenced by:  alimi  1654  al2imi  1657  albii  1661  eximi  1677  exbii  1688  spfw  1830  hbn  1923  chvar  2040  equsb1  2131  equsb2  2132  nfsb4  2155  sbt  2186  sbtr  2188  moimi  2292  2eumo  2318  vtoclf  3110  vtocl2  3112  vtocl3  3113  spcimgf  3137  spcgf  3139  euxfr2  3234  axsep  4516  axnulALT  4523  csbex  4529  eusv2nf  4592  dtrucor  4624  ssopab2i  4718  iotabii  5555  opabiotafun  5910  eufnfv  6127  tz9.13  8241  unir1  8263  axac2  8878  axpowndlem3  9006  uzrdgfni  12110  setinds  29997  hbng  30028  bj-axd2d  30745  bj-nffal  30765  bj-nfxfr  30782  bj-hbsb3  30837  bj-nfs1  30840  bj-chvarv  30850  bj-equsb1v  30907  bj-sbtv  30911  bj-axsep  30943  bj-dtrucor  30950  bj-vexw  30995  bj-vexwv  30997  bj-issetw  31000  bj-abf  31039  bj-vtoclf  31044  bj-snsetex  31086  ax4  31918  ax10  31919  ax6fromc10  31920  equid1  31930  setindtrs  35329  frege97  35941  frege109  35953  pm11.11  36127  sbeqal1i  36153  axc5c4c711toc7  36159  axc5c4c711to11  36160  iotaequ  36184