Theorem mpg 1724

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 1722	. 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 1481

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

This theorem is referenced by:  nfth  1727  nfnth  1728  alimi  1739  al2imi  1743  albii  1747  eximi  1762  exbii  1774  nfbii  1778  exanOLD  1789  spfwOLD  1966  nf5i  2024  hbn  2146  chvar  2262  chvarv  2263  equsb1  2368  equsb2  2369  nfsb4  2390  sbt  2419  sbtr  2421  moimi  2520  2eumo  2545  vtoclf  3258  vtocl  3259  vtocl2  3261  vtocl3  3262  spcimgf  3286  spcgf  3288  euxfr2  3391  axsep  4780  axnulALT  4787  csbex  4793  eusv2nf  4864  dtrucor  4900  ssopab2i  5003  iotabii  5873  opabiotafun  6259  eufnfv  6491  snnex  6966  pwnex  6968  tz9.13  8654  unir1  8676  axac2  9288  axpowndlem3  9421  uzrdgfni  12757  uvtxa01vtx0  26297  setinds  31683  hbng  31714  bj-axd2d  32577  bj-exalimsi  32614  bj-ssbimi  32623  bj-ssbbii  32624  bj-hbsb3  32713  bj-nfs1  32716  bj-chvarv  32725  bj-chvarvv  32726  bj-equsb1v  32762  bj-sbtv  32766  bj-axsep  32793  bj-dtrucor  32800  bj-vexw  32855  bj-vexwv  32857  bj-issetw  32860  bj-abf  32903  bj-vtoclf  32908  bj-snsetex  32951  ax4fromc4  34179  ax10fromc7  34180  ax6fromc10  34181  equid1  34184  setindtrs  37592  frege97  38254  frege109  38266  pm11.11  38573  sbeqal1i  38599  axc5c4c711toc7  38605  axc5c4c711to11  38606  iotaequ  38630  setrec2lem2  42441  vsetrec  42446