Theorem mpg 1564

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 1562	. 2
3		mpg.1	. 2
4	2, 3	ax-mp 5	1

Syntax hints:  ->wi 4  A.wal 1556

This theorem is referenced by:  alimi  1575  albii  1582  eximi  1594  exbii  1601  spfw  1710  spwOLD  1712  19.9hOLD  1794  hbn  1800  chvar  1967  chvarvOLD  1969  cbv3hOLD  1976  cbv3OLD  1977  sbt  2093  equsb1  2103  equsb2  2104  nfsb4  2131  ax4  2248  ax10  2249  ax6fromc10  2250  equid1  2260  moimi  2365  2eumo  2398  vtoclf  3055  vtocl2  3057  vtocl3  3058  spcimgf  3079  spcgf  3081  euxfr2  3170  axsep  4422  axnulALT  4429  csbex  4435  csbexOLD  4437  eusv2nf  4497  dtrucor  4532  ssopab2i  4621  iotabii  5402  opabiotafun  5745  eufnfv  5929  tz9.13  7829  unir1  7851  axac2  8460  axpowndlem3  8588  uzrdgfni  11573  setinds  26235  hbng  26266  setindtrs  28025  pm11.11  28475  sbeqal1i  28501  axc5c4c711toc7  28507  axc5c4c711to11  28508  iotaequ  28532  bj-snsetex  30670  cbv3wAUX11  30792  equsb1NEW11  30813  equsb2NEW11  30814  nfsb4wAUX11  30852  chvarNEW11  30894  chvarvNEW11  30900  cbv3OLD11  30997  cbv3hOLD11  30998  nfsb4OLD11  31021

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