Theorem mpg 1799

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

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  nfth  1803  nfnth  1804  alimi  1813  al2imi  1817  albii  1821  eximi  1837  exbii  1850  nfbii  1854  chvarvv  1991  sbtALT  2075  sbn1  2113  nf5i  2152  chvarfv  2248  hbn  2302  chvar  2400  equsb1  2496  equsb2  2497  nfsb4  2505  sbtr  2521  moimi  2546  mobii  2549  eubii  2586  2eumo  2643  abbii  2804  spcimgf  3508  spcgf  3546  euxfr2w  3679  euxfr2  3681  noel  4291  axsepgfromrep  5240  axnulALT  5250  csbex  5257  dtrucor  5317  eusv2nf  5341  axprlem3  5371  axprlem3OLD  5374  ssopab2i  5499  iotabii  6478  opabiotafun  6915  eufnfv  7177  snnex  7705  pwnex  7706  setinds  9662  tz9.13  9707  unir1  9729  axac2  10380  axpowndlem3  10514  uzrdgfni  13885  uvtx01vtx  29453  setinds2regs  35268  unir1regs  35272  hbng  35981  bj-axd2d  36768  bj-exalimsi  36810  bj-hbsb3  36965  bj-nfs1  36968  sbn1ALT  37034  bj-issetw  37052  bj-abf  37085  bj-vtoclf  37091  bj-snsetex  37139  ax4fromc4  39191  ax10fromc7  39192  ax6fromc10  39193  equid1  39196  sn-axprlem3  42511  setindtrs  43303  frege97  44237  frege109  44249  pm11.11  44651  sbeqal1i  44676  axc5c4c711toc7  44681  axc5c4c711to11  44682  iotaequ  44706  mof0  49119  setrec2lem2  49975  vsetrec  49984