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  2814  vtocl2  2816  vtocl3  2817  spcimgf  2841  spcimegf  2842  spcgf  2843  spcegf  2844  mosub  2939  csbexa  4159  nalset  4160  ssopab2i  4309  pwnex  4481  eusv2nf  4488  iotabii  5239  fvmptss2  5633  eufnfv  5790  riotaexg  5878  xpcomco  6882  bj-ex  15324  ch2var  15329  bj-vtoclgf  15338  elabgf1  15341  bj-rspg  15349  sumdc2  15361  bdsepnf  15450  bj-nalset  15457  setindf  15528  strcollnf  15547