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  7178  snnex  7706  pwnex  7707  setinds  9663  tz9.13  9708  unir1  9730  axac2  10381  axpowndlem3  10515  uzrdgfni  13886  uvtx01vtx  29475  setinds2regs  35300  unir1regs  35304  hbng  36013  bj-axd2d  36806  bj-exalimsi  36848  bj-hbsb3  37003  bj-nfs1  37006  sbn1ALT  37072  bj-issetw  37090  bj-abf  37123  bj-vtoclf  37129  bj-snsetex  37177  ax4fromc4  39233  ax10fromc7  39234  ax6fromc10  39235  equid1  39238  sn-axprlem3  42553  setindtrs  43345  frege97  44279  frege109  44291  pm11.11  44693  sbeqal1i  44718  axc5c4c711toc7  44723  axc5c4c711to11  44724  iotaequ  44748  mof0  49160  setrec2lem2  50016  vsetrec  50025