Theorem mpg 1572

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

Syntax hints:  ->wi 4  A.wal 1564

This theorem is referenced by:  alimi  1583  albii  1590  eximi  1602  exbii  1609  spfw  1718  spwOLD  1720  19.9hOLD  1802  hbn  1808  chvar  1975  chvarvOLD  1977  cbv3hOLD  1984  cbv3OLD  1985  sbt  2101  equsb1  2111  equsb2  2112  nfsb4  2139  ax4  2256  ax10  2257  ax6fromc10  2258  equid1  2268  moimi  2373  2eumo  2406  vtoclf  3064  vtocl2  3066  vtocl3  3067  spcimgf  3090  spcgf  3092  euxfr2  3182  axsep  4438  axnulALT  4445  csbex  4451  csbexOLD  4453  eusv2nf  4513  dtrucor  4548  ssopab2i  4639  iotabii  5423  opabiotafun  5768  eufnfv  5965  tz9.13  7884  unir1  7906  axac2  8517  axpowndlem3  8645  uzrdgfni  11630  setinds  26744  hbng  26775  setindtrs  28522  pm11.11  28800  sbeqal1i  28826  axc5c4c711toc7  28832  axc5c4c711to11  28833  iotaequ  28857  bj-snsetex  30947  cbv3wAUX11  31069  equsb1NEW11  31090  equsb2NEW11  31091  nfsb4wAUX11  31129  chvarNEW11  31171  chvarvNEW11  31177  cbv3OLD11  31274  cbv3hOLD11  31275  nfsb4OLD11  31298

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