Theorem mpg 1620

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

Syntax hints:  ->wi 4  A.wal 1393

This theorem is referenced by:  alimi  1633  al2imi  1636  albii  1640  eximi  1656  exbii  1667  spfw  1806  hbn  1895  chvar  2013  equsb1  2107  equsb2  2108  nfsb4  2131  sbt  2162  sbtr  2164  ax4  2225  ax10  2226  ax6fromc10  2227  equid1  2237  moimi  2340  2eumo  2367  vtoclf  3160  vtocl2  3162  vtocl3  3163  spcimgf  3187  spcgf  3189  euxfr2  3284  axsep  4572  axnulALT  4579  csbex  4585  csbexOLD  4587  eusv2nf  4650  dtrucor  4685  ssopab2i  4780  iotabii  5578  opabiotafun  5934  eufnfv  6146  tz9.13  8230  unir1  8252  axac2  8867  axpowndlem3  8996  axpowndlem3OLD  8997  uzrdgfni  12069  setinds  29210  hbng  29241  setindtrs  30967  pm11.11  31279  sbeqal1i  31305  axc5c4c711toc7  31311  axc5c4c711to11  31312  iotaequ  31336  bj-axd2d  34181  bj-nffal  34201  bj-nfxfr  34218  bj-hbsb3  34273  bj-nfs1  34276  bj-chvarv  34286  bj-equsb1v  34343  bj-sbtv  34347  bj-axsep  34379  bj-dtrucor  34386  bj-vexw  34431  bj-vexwv  34433  bj-issetw  34436  bj-abf  34475  bj-vtoclf  34480  bj-snsetex  34521

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