Theorem mpg 1428

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 1426	. 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 1330

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

This theorem is referenced by:  alimi  1432  albii  1447  a5i  1523  eximi  1580  exbii  1585  19.9h  1623  hbn  1633  chvar  1731  equsb1  1759  equsb2  1760  chvarvv  1881  chvarv  1910  moimi  2065  2eumo  2088  vtoclf  2742  vtocl2  2744  vtocl3  2745  spcimgf  2769  spcimegf  2770  spcgf  2771  spcegf  2772  mosub  2866  csbexa  4065  nalset  4066  ssopab2i  4207  pwnex  4378  eusv2nf  4385  iotabii  5118  fvmptss2  5504  eufnfv  5656  riotaexg  5742  xpcomco  6728  bj-ex  13140  ch2var  13145  bj-vtoclgf  13154  elabgf1  13157  bj-rspg  13165  sumdc2  13177  bdsepnf  13257  bj-nalset  13264  setindf  13335  strcollnf  13354