Theorem mpg 1603

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 1601	. 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 1377

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

This theorem is referenced by:  alimi  1614  albii  1620  eximi  1635  exbii  1644  spfw  1755  hbn  1843  chvar  1982  cbv3hOLD  1990  equsb1  2080  equsb2  2081  nfsb4  2104  sbt  2140  sbtr  2142  ax4  2218  ax10  2219  ax6fromc10  2220  equid1  2230  moimi  2342  2eumo  2376  vtoclf  3164  vtocl2  3166  vtocl3  3167  spcimgf  3191  spcgf  3193  euxfr2  3288  axsep  4567  axnulALT  4574  csbex  4580  csbexOLD  4582  eusv2nf  4645  dtrucor  4680  ssopab2i  4775  iotabii  5571  opabiotafun  5926  eufnfv  6132  tz9.13  8205  unir1  8227  axac2  8842  axpowndlem3  8971  axpowndlem3OLD  8972  uzrdgfni  12033  setinds  28787  hbng  28818  setindtrs  30571  pm11.11  30857  sbeqal1i  30883  axc5c4c711toc7  30889  axc5c4c711to11  30890  iotaequ  30914  bj-axd2d  33263  bj-nffal  33284  bj-nfxfr  33306  bj-hbsb3  33355  bj-nfs1  33358  bj-chvarv  33368  bj-equsb1v  33424  bj-sbtv  33428  bj-axsep  33460  bj-dtrucor  33467  bj-vexw  33512  bj-vexwv  33514  bj-issetw  33517  bj-abf  33556  bj-vtoclf  33561  bj-snsetex  33602