Theorem mpg 1462

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 1460	. 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 1362

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

This theorem is referenced by:  alimi  1466  albii  1481  a5i  1554  nfal  1587  eximi  1611  exbii  1616  19.9h  1654  hbn  1665  chvarfv  1711  chvar  1768  equsb1  1796  equsb2  1797  chvarvv  1920  chvarv  1953  moimi  2107  2eumo  2130  vtoclf  2813  vtocl2  2815  vtocl3  2816  spcimgf  2840  spcimegf  2841  spcgf  2842  spcegf  2843  mosub  2938  csbexa  4158  nalset  4159  ssopab2i  4308  pwnex  4480  eusv2nf  4487  iotabii  5238  fvmptss2  5632  eufnfv  5789  riotaexg  5877  xpcomco  6880  bj-ex  15254  ch2var  15259  bj-vtoclgf  15268  elabgf1  15271  bj-rspg  15279  sumdc2  15291  bdsepnf  15380  bj-nalset  15387  setindf  15458  strcollnf  15477