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  3496  spcgf  3534  euxfr2w  3667  euxfr2  3669  noel  4279  axsepgfromrep  5229  axnulALT  5239  csbex  5246  dtrucor  5306  eusv2nf  5330  axprlem3  5360  axprlem3OLD  5364  ssopab2i  5496  iotabii  6475  opabiotafun  6912  eufnfv  7175  snnex  7703  pwnex  7704  setinds  9659  tz9.13  9704  unir1  9726  axac2  10377  axpowndlem3  10511  uzrdgfni  13882  uvtx01vtx  29454  axnulALT2  35230  setinds2regs  35281  unir1regs  35285  hbng  35994  bj-axd2d  36856  bj-exalimsi  36911  bj-hbal  36976  bj-hbsb3  37094  bj-nfs1  37097  sbn1ALT  37163  bj-issetw  37181  bj-abf  37214  bj-vtoclf  37220  bj-snsetex  37268  ax4fromc4  39331  ax10fromc7  39332  ax6fromc10  39333  equid1  39336  sn-axprlem3  42651  setindtrs  43456  frege97  44390  frege109  44402  pm11.11  44804  sbeqal1i  44829  axc5c4c711toc7  44834  axc5c4c711to11  44835  iotaequ  44859  mof0  49271  setrec2lem2  50127  vsetrec  50136