Theorem mpg 1451

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 1449	. 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 1351

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

This theorem is referenced by:  alimi  1455  albii  1470  a5i  1543  nfal  1576  eximi  1600  exbii  1605  19.9h  1643  hbn  1654  chvarfv  1700  chvar  1757  equsb1  1785  equsb2  1786  chvarvv  1908  chvarv  1937  moimi  2091  2eumo  2114  vtoclf  2791  vtocl2  2793  vtocl3  2794  spcimgf  2818  spcimegf  2819  spcgf  2820  spcegf  2821  mosub  2916  csbexa  4133  nalset  4134  ssopab2i  4278  pwnex  4450  eusv2nf  4457  iotabii  5201  fvmptss2  5592  eufnfv  5748  riotaexg  5835  xpcomco  6826  bj-ex  14517  ch2var  14522  bj-vtoclgf  14531  elabgf1  14534  bj-rspg  14542  sumdc2  14554  bdsepnf  14643  bj-nalset  14650  setindf  14721  strcollnf  14740