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  2247  hbn  2301  chvar  2398  equsb1  2494  equsb2  2495  nfsb4  2503  sbtr  2519  moimi  2544  mobii  2547  eubii  2584  2eumo  2641  abbii  2802  spcimgf  3493  spcgf  3531  euxfr2w  3663  euxfr2  3665  noel  4268  axsepgfromrep  5218  axnulALT  5228  csbex  5235  dtrucor  5302  eusv2nf  5326  axprlem3  5356  axprlem3OLD  5360  ssopab2i  5494  iotabii  6472  opabiotafun  6909  eufnfv  7173  snnex  7701  pwnex  7702  setinds  9659  tz9.13  9704  unir1  9726  axac2  10377  axpowndlem3  10511  uzrdgfni  13909  uvtx01vtx  29454  axnulALT2  35212  setinds2regs  35263  unir1regs  35267  hbng  35976  bj-axd2d  36846  bj-exalimsi  36901  bj-hbal  36966  bj-hbsb3  37084  bj-nfs1  37087  sbn1ALT  37153  bj-issetw  37171  bj-abf  37204  bj-vtoclf  37210  bj-snsetex  37258  ax4fromc4  39328  ax10fromc7  39329  ax6fromc10  39330  equid1  39333  sn-axprlem3  42647  setindtrs  43441  frege97  44375  frege109  44387  pm11.11  44789  sbeqal1i  44814  axc5c4c711toc7  44819  axc5c4c711to11  44820  iotaequ  44844  mof0  49301  setrec2lem2  50157  vsetrec  50166