Theorem mpg 1721

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

Syntax hints:   → wi 4  ∀wal 1478

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

This theorem is referenced by:  nfth  1724  nfnth  1725  alimi  1736  al2imi  1740  albii  1744  eximi  1759  exbii  1771  nfbii  1775  exanOLD  1786  spfwOLD  1963  nf5i  2021  hbn  2142  chvar  2261  chvarv  2262  equsb1  2367  equsb2  2368  nfsb4  2389  sbt  2418  sbtr  2420  moimi  2519  2eumo  2544  vtoclf  3248  vtocl  3249  vtocl2  3251  vtocl3  3252  spcimgf  3276  spcgf  3278  euxfr2  3378  axsep  4750  axnulALT  4757  csbex  4763  eusv2nf  4834  dtrucor  4871  ssopab2i  4973  iotabii  5842  opabiotafun  6226  eufnfv  6456  snnex  6930  pwnex  6932  tz9.13  8614  unir1  8636  axac2  9248  axpowndlem3  9381  uzrdgfni  12713  uvtxa01vtx0  26218  setinds  31437  hbng  31468  bj-axd2d  32272  bj-exalimsi  32309  bj-ssbimi  32318  bj-ssbbii  32319  bj-hbsb3  32408  bj-nfs1  32411  bj-chvarv  32420  bj-chvarvv  32421  bj-equsb1v  32458  bj-sbtv  32462  bj-axsep  32489  bj-dtrucor  32496  bj-vexw  32555  bj-vexwv  32557  bj-issetw  32560  bj-abf  32603  bj-vtoclf  32608  bj-snsetex  32651  ax4fromc4  33698  ax10fromc7  33699  ax6fromc10  33700  equid1  33703  setindtrs  37111  frege97  37775  frege109  37787  pm11.11  38094  sbeqal1i  38120  axc5c4c711toc7  38126  axc5c4c711to11  38127  iotaequ  38151  setrec2lem2  41764  vsetrec  41769