Theorem mpg 1797

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

Syntax hints:   → wi 4  ∀wal 1538

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

This theorem is referenced by:  nfth  1801  nfnth  1802  alimi  1811  al2imi  1815  albii  1819  eximi  1835  exbii  1848  nfbii  1852  chvarvv  1989  sbtALT  2070  sbn1  2108  nf5i  2147  chvarfv  2241  hbn  2296  chvar  2400  equsb1  2496  equsb2  2497  nfsb4  2505  sbtr  2521  2eumo  2642  abbii  2803  spcimgf  3534  vtoclfOLD  3549  spcgf  3575  euxfr2w  3708  euxfr2  3710  noel  4318  axsepgfromrep  5269  axnulALT  5279  csbex  5286  dtrucor  5346  eusv2nf  5370  axprlem3  5400  axprlem3OLD  5403  ssopab2i  5530  iotabii  6521  opabiotafun  6964  eufnfv  7226  snnex  7757  pwnex  7758  tz9.13  9810  unir1  9832  axac2  10485  axpowndlem3  10618  uzrdgfni  13981  uvtx01vtx  29381  setinds  35801  hbng  35831  bj-axd2d  36616  bj-exalimsi  36658  bj-hbsb3  36812  bj-nfs1  36815  sbn1ALT  36881  bj-issetw  36899  bj-abf  36932  bj-vtoclf  36938  bj-snsetex  36986  ax4fromc4  38917  ax10fromc7  38918  ax6fromc10  38919  equid1  38922  sn-axprlem3  42235  setindtrs  43024  frege97  43959  frege109  43971  pm11.11  44373  sbeqal1i  44398  axc5c4c711toc7  44403  axc5c4c711to11  44404  iotaequ  44428  mof0  48796  setrec2lem2  49538  vsetrec  49547