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  2792  vtocl2  2794  vtocl3  2795  spcimgf  2819  spcimegf  2820  spcgf  2821  spcegf  2822  mosub  2917  csbexa  4134  nalset  4135  ssopab2i  4279  pwnex  4451  eusv2nf  4458  iotabii  5202  fvmptss2  5594  eufnfv  5750  riotaexg  5838  xpcomco  6829  bj-ex  14702  ch2var  14707  bj-vtoclgf  14716  elabgf1  14719  bj-rspg  14727  sumdc2  14739  bdsepnf  14828  bj-nalset  14835  setindf  14906  strcollnf  14925