Theorem mpg 1797

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 1795	. 2 ⊢ ∀𝑥𝜑
3		mpg.1	. 2 ⊢ (∀𝑥𝜑 → 𝜓)
4	2, 3	ax-mp 5	1 ⊢ 𝜓

Syntax hints:   → wi 4  ∀wal 1538

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

This theorem is referenced by:  nfth  1801  nfnth  1802  alimi  1811  al2imi  1815  albii  1819  eximi  1835  exbii  1848  nfbii  1852  chvarvv  1989  sbtALT  2070  sbn1  2108  nf5i  2147  chvarfv  2241  hbn  2295  chvar  2393  equsb1  2489  equsb2  2490  nfsb4  2498  sbtr  2514  2eumo  2635  abbii  2796  spcimgf  3516  vtoclfOLD  3531  spcgf  3557  euxfr2w  3691  euxfr2  3693  noel  4301  axsepgfromrep  5249  axnulALT  5259  csbex  5266  dtrucor  5326  eusv2nf  5350  axprlem3  5380  axprlem3OLD  5383  ssopab2i  5510  iotabii  6496  opabiotafun  6941  eufnfv  7203  snnex  7734  pwnex  7735  tz9.13  9744  unir1  9766  axac2  10419  axpowndlem3  10552  uzrdgfni  13923  uvtx01vtx  29324  setinds  35766  hbng  35796  bj-axd2d  36581  bj-exalimsi  36623  bj-hbsb3  36777  bj-nfs1  36780  sbn1ALT  36846  bj-issetw  36864  bj-abf  36897  bj-vtoclf  36903  bj-snsetex  36951  ax4fromc4  38887  ax10fromc7  38888  ax6fromc10  38889  equid1  38892  sn-axprlem3  42205  setindtrs  43014  frege97  43949  frege109  43961  pm11.11  44363  sbeqal1i  44388  axc5c4c711toc7  44393  axc5c4c711to11  44394  iotaequ  44418  mof0  48826  setrec2lem2  49683  vsetrec  49692