Theorem mpg 1337

Description: Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.)

Hypotheses

Ref	Expression
mpg.1	|- (A.xph -> 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 1335	. 2 |- A.xph
3		mpg.1	. 2 |- (A.xph -> ps)
4	2, 3	ax-mp 7	1 |- ps

Syntax hints:   -> wi 4  A.wal 1240

This theorem was proved from axioms:  ax-mp 7  ax-gen 1335

This theorem is referenced by:  alimi  1341  albii  1356  a5i  1432  eximi  1488  exbii  1493  19.9h  1531  hbn  1541  chvar  1637  equsb1  1665  equsb2  1666  chvarv  1809  moimi  1962  2eumo  1985  vtoclf  2601  vtocl2  2603  vtocl3  2604  spcimgf  2627  spcimegf  2628  spcgf  2629  spcegf  2630  mosub  2713  csbexa  3877  nalset  3878  ssopab2i  4005  eusv2nf  4154  iotabii  4832  fvmptss2  5190  eufnfv  5332  riotaexg  5415  xpcomco  6236  bj-ex  9237  ch2var  9242  bj-vtoclgf  9250  elabgf1  9253  bj-rspg  9261  bdsepnf  9343  bj-nalset  9350  setindf  9426  strcollnf  9445