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  13909  uvtx01vtx  29485  axnulALT2  35245  setinds2regs  35296  unir1regs  35300  hbng  36009  bj-axd2d  36871  bj-exalimsi  36926  bj-hbal  36991  bj-hbsb3  37109  bj-nfs1  37112  sbn1ALT  37178  bj-issetw  37196  bj-abf  37229  bj-vtoclf  37235  bj-snsetex  37283  ax4fromc4  39351  ax10fromc7  39352  ax6fromc10  39353  equid1  39356  sn-axprlem3  42670  setindtrs  43468  frege97  44402  frege109  44414  pm11.11  44816  sbeqal1i  44841  axc5c4c711toc7  44846  axc5c4c711to11  44847  iotaequ  44871  mof0  49310  setrec2lem2  50166  vsetrec  50175