Theorem mpg 1427

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 1425	. 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 1329

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

This theorem is referenced by:  alimi  1431  albii  1446  a5i  1522  eximi  1579  exbii  1584  19.9h  1622  hbn  1632  chvar  1730  equsb1  1758  equsb2  1759  chvarvv  1880  chvarv  1907  moimi  2062  2eumo  2085  vtoclf  2734  vtocl2  2736  vtocl3  2737  spcimgf  2761  spcimegf  2762  spcgf  2763  spcegf  2764  mosub  2857  csbexa  4052  nalset  4053  ssopab2i  4194  pwnex  4365  eusv2nf  4372  iotabii  5105  fvmptss2  5489  eufnfv  5641  riotaexg  5727  xpcomco  6713  bj-ex  12958  ch2var  12963  bj-vtoclgf  12972  elabgf1  12975  bj-rspg  12983  sumdc2  12995  bdsepnf  13075  bj-nalset  13082  setindf  13153  strcollnf  13172