Theorem mpg 1554

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 1552	. 2 |- A. x ph
3		mpg.1	. 2 |- ( A. x ph -> ps )
4	2, 3	ax-mp 8	1 |- ps

Syntax hints:   -> wi 4   A.wal 1546

This theorem is referenced by:  alimi  1565  albii  1572  eximi  1582  exbii  1589  spfw  1699  spwOLD  1703  19.9hOLD  1791  hbn  1797  cbv3  2035  cbv3h  2036  chvar  2039  chvarv  2063  equsb1  2083  equsb2  2084  nfsb4  2130  ax5  2196  ax6  2197  ax9from9o  2198  equid1  2208  moimi  2301  2eumo  2327  vtoclf  2965  vtocl2  2967  vtocl3  2968  spcimgf  2989  spcgf  2991  euxfr2  3079  csbex  3222  axsep  4289  axnulALT  4296  dtrucor  4357  ssopab2i  4442  eusv2nf  4680  iotabii  5399  eufnfv  5931  opabiotafun  6495  tz9.13  7673  unir1  7695  axac2  8302  axpowndlem3  8430  uzrdgfni  11253  setinds  25348  hbng  25379  setindtrs  26986  pm11.11  27438  sbeqal1i  27466  ax4567to6  27472  ax4567to7  27473  iotaequ  27497  cbv3wAUX7  29221  equsb1NEW7  29242  equsb2NEW7  29243  nfsb4wAUX7  29281  chvarNEW7  29321  chvarvNEW7  29327  cbv3OLD7  29407  cbv3hOLD7  29408  nfsb4OLD7  29431

This theorem was proved from axioms:  ax-mp 8  ax-gen 1552