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

Step	Hyp	Ref	Expression
1		mpg.2	. . 3 |- ph
2	1	ax-gen 1666	. 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 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