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  1805  equsb1  1833  equsb2  1834  chvarvv  1957  chvarv  1990  moimi  2145  2eumo  2168  vtoclf  2858  vtocl2  2860  vtocl3  2861  spcimgf  2887  spcimegf  2888  spcgf  2889  spcegf  2890  mosub  2985  csbexa  4223  nalset  4224  ssopab2i  4378  pwnex  4552  eusv2nf  4559  iotabii  5317  fvmptss2  5730  eufnfv  5895  riotaexg  5985  xpcomco  7053  bj-ex  16480  ch2var  16485  bj-vtoclgf  16494  elabgf1  16497  bj-rspg  16505  sumdc2  16517  bdsepnf  16604  bj-nalset  16611  setindf  16682  strcollnf  16701