Theorem mpg 1558

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

Hypotheses

Ref	Expression
mpg.1
mpg.2

Assertion

Ref	Expression
mpg

Proof of Theorem mpg

Step	Hyp	Ref	Expression
1		mpg.2	. . 3
2	1	ax-gen 1556	. 2
3		mpg.1	. 2
4	2, 3	ax-mp 5	1

Syntax hints:  ->wi 4  A.wal 1550

This theorem is referenced by:  alimi  1569  albii  1576  eximi  1586  exbii  1593  spfw  1706  spwOLD  1710  19.9hOLD  1798  hbn  1804  chvar  1972  chvarvOLD  1974  cbv3hOLD  1981  cbv3OLD  1982  sbt  2096  equsb1  2106  equsb2  2107  nfsb4  2134  ax5  2230  ax6  2231  ax9from9o  2232  equid1  2242  moimi  2335  2eumo  2361  vtoclf  3014  vtocl2  3016  vtocl3  3017  spcimgf  3038  spcgf  3040  euxfr2  3128  axsep  4363  axnulALT  4370  csbex  4376  csbexOLD  4378  dtrucor  4436  ssopab2i  4521  eusv2nf  4762  iotabii  5486  eufnfv  6020  opabiotafun  6586  tz9.13  7766  unir1  7788  axac2  8397  axpowndlem3  8525  uzrdgfni  11349  setinds  25509  hbng  25540  setindtrs  27275  pm11.11  27726  sbeqal1i  27754  ax4567to6  27760  ax4567to7  27761  iotaequ  27785  cbv3wAUX7  29758  equsb1NEW7  29779  equsb2NEW7  29780  nfsb4wAUX7  29818  chvarNEW7  29861  chvarvNEW7  29867  cbv3OLD7  29964  cbv3hOLD7  29965  nfsb4OLD7  29988

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