Theorem mpg 1500

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 1498	. 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 1396

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

This theorem is referenced by:  alimi  1504  albii  1519  a5i  1592  nfal  1625  eximi  1649  exbii  1654  19.9h  1692  hbnOLD  1702  chvarfv  1748  chvar  1806  equsb1  1834  equsb2  1835  chvarvv  1960  chvarv  1993  moimi  2148  2eumo  2171  vtoclf  2870  vtocl2  2872  vtocl3  2873  spcimgf  2899  spcimegf  2900  spcgf  2901  spcegf  2902  mosub  2997  csbexa  4241  nalset  4242  ssopab2i  4398  pwnex  4572  eusv2nf  4579  iotabii  5338  fvmptss2  5754  eufnfv  5919  riotaexg  6009  xpcomco  7079  bj-ex  16583  ch2var  16588  bj-vtoclgf  16597  elabgf1  16600  bj-rspg  16608  sumdc2  16620  bdsepnf  16707  bj-nalset  16714  setindf  16785  strcollnf  16804