Theorem mpg 1465

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 1463	. 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 1463

This theorem is referenced by:  alimi  1469  albii  1484  a5i  1557  nfal  1590  eximi  1614  exbii  1619  19.9h  1657  hbn  1668  chvarfv  1714  chvar  1771  equsb1  1799  equsb2  1800  chvarvv  1923  chvarv  1956  moimi  2110  2eumo  2133  vtoclf  2817  vtocl2  2819  vtocl3  2820  spcimgf  2844  spcimegf  2845  spcgf  2846  spcegf  2847  mosub  2942  csbexa  4163  nalset  4164  ssopab2i  4313  pwnex  4485  eusv2nf  4492  iotabii  5243  fvmptss2  5639  eufnfv  5796  riotaexg  5884  xpcomco  6894  bj-ex  15492  ch2var  15497  bj-vtoclgf  15506  elabgf1  15509  bj-rspg  15517  sumdc2  15529  bdsepnf  15618  bj-nalset  15625  setindf  15696  strcollnf  15715