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  4162  nalset  4163  ssopab2i  4312  pwnex  4484  eusv2nf  4491  iotabii  5242  fvmptss2  5636  eufnfv  5793  riotaexg  5881  xpcomco  6885  bj-ex  15408  ch2var  15413  bj-vtoclgf  15422  elabgf1  15425  bj-rspg  15433  sumdc2  15445  bdsepnf  15534  bj-nalset  15541  setindf  15612  strcollnf  15631