Theorem mpg 1798

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

Syntax hints:   → wi 4  ∀wal 1535

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

This theorem is referenced by:  nfth  1802  nfnth  1803  alimi  1812  al2imi  1816  albii  1820  eximi  1835  exbii  1848  nfbii  1852  chvarvv  2005  sbtALT  2074  equsb1vOLD  2113  nf5i  2150  chvarfv  2242  hbn  2303  chvar  2413  equsb1  2530  equsb2  2531  nfsb4  2540  sbtr  2558  equsb1ALT  2601  nfsb4ALT  2605  moimiOLD  2628  mobiiOLD  2632  eubiiOLD  2671  2eumo  2727  abbii  2888  vtoclf  3560  vtocl2OLD  3564  spcimgf  3590  spcgf  3592  euxfr2w  3713  euxfr2  3715  axsepgfromrep  5203  axnulALT  5210  csbex  5217  dtrucor  5274  eusv2nf  5298  axprlem3  5328  ssopab2i  5439  iotabii  6342  opabiotafun  6746  eufnfv  6993  snnex  7482  pwnex  7483  tz9.13  9222  unir1  9244  axac2  9890  axpowndlem3  10023  uzrdgfni  13329  uvtx01vtx  27181  setinds  33025  hbng  33055  bj-axd2d  33929  bj-exalimsi  33970  bj-hbsb3  34113  bj-nfs1  34116  bj-issetw  34192  bj-abf  34227  bj-vtoclf  34233  bj-snsetex  34277  ax4fromc4  36032  ax10fromc7  36033  ax6fromc10  36034  equid1  36037  sn-axprlem3  39116  setindtrs  39629  frege97  40313  frege109  40325  pm11.11  40713  sbeqal1i  40738  axc5c4c711toc7  40743  axc5c4c711to11  40744  iotaequ  40768  setrec2lem2  44804  vsetrec  44812