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  2295  chvar  2393  equsb1  2489  equsb2  2490  nfsb4  2498  sbtr  2514  2eumo  2635  abbii  2796  spcimgf  3507  vtoclfOLD  3522  spcgf  3548  euxfr2w  3682  euxfr2  3684  noel  4291  axsepgfromrep  5236  axnulALT  5246  csbex  5253  dtrucor  5313  eusv2nf  5337  axprlem3  5367  axprlem3OLD  5370  ssopab2i  5497  iotabii  6471  opabiotafun  6907  eufnfv  7169  snnex  7698  pwnex  7699  tz9.13  9706  unir1  9728  axac2  10379  axpowndlem3  10512  uzrdgfni  13883  uvtx01vtx  29360  setinds2regs  35065  unir1regs  35067  setinds  35751  hbng  35781  bj-axd2d  36566  bj-exalimsi  36608  bj-hbsb3  36762  bj-nfs1  36765  sbn1ALT  36831  bj-issetw  36849  bj-abf  36882  bj-vtoclf  36888  bj-snsetex  36936  ax4fromc4  38872  ax10fromc7  38873  ax6fromc10  38874  equid1  38877  sn-axprlem3  42190  setindtrs  42998  frege97  43933  frege109  43945  pm11.11  44347  sbeqal1i  44372  axc5c4c711toc7  44377  axc5c4c711to11  44378  iotaequ  44402  mof0  48810  setrec2lem2  49667  vsetrec  49676