Theorem mpg 1477

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 1475	. 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 1373

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

This theorem is referenced by:  alimi  1481  albii  1496  a5i  1569  nfal  1602  eximi  1626  exbii  1631  19.9h  1669  hbn  1680  chvarfv  1726  chvar  1783  equsb1  1811  equsb2  1812  chvarvv  1935  chvarv  1968  moimi  2123  2eumo  2146  vtoclf  2834  vtocl2  2836  vtocl3  2837  spcimgf  2863  spcimegf  2864  spcgf  2865  spcegf  2866  mosub  2961  csbexa  4192  nalset  4193  ssopab2i  4345  pwnex  4517  eusv2nf  4524  iotabii  5278  fvmptss2  5682  eufnfv  5843  riotaexg  5931  xpcomco  6953  bj-ex  16036  ch2var  16041  bj-vtoclgf  16050  elabgf1  16053  bj-rspg  16061  sumdc2  16073  bdsepnf  16161  bj-nalset  16168  setindf  16239  strcollnf  16258