Theorem mpg 1499

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 1497	. 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 1395

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

This theorem is referenced by:  alimi  1503  albii  1518  a5i  1591  nfal  1624  eximi  1648  exbii  1653  19.9h  1691  hbnOLD  1701  chvarfv  1747  chvar  1804  equsb1  1832  equsb2  1833  chvarvv  1956  chvarv  1989  moimi  2144  2eumo  2167  vtoclf  2856  vtocl2  2858  vtocl3  2859  spcimgf  2885  spcimegf  2886  spcgf  2887  spcegf  2888  mosub  2983  csbexa  4219  nalset  4220  ssopab2i  4374  pwnex  4548  eusv2nf  4555  iotabii  5312  fvmptss2  5724  eufnfv  5890  riotaexg  5980  xpcomco  7015  bj-ex  16419  ch2var  16424  bj-vtoclgf  16433  elabgf1  16436  bj-rspg  16444  sumdc2  16456  bdsepnf  16543  bj-nalset  16550  setindf  16621  strcollnf  16640