Theorem mpg 1798

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

Syntax hints:   → wi 4  ∀wal 1539

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

This theorem is referenced by:  nfth  1802  nfnth  1803  alimi  1812  al2imi  1816  albii  1820  eximi  1836  exbii  1849  nfbii  1853  chvarvv  1990  sbtALT  2072  sbn1  2110  nf5i  2149  chvarfv  2243  hbn  2297  chvar  2395  equsb1  2491  equsb2  2492  nfsb4  2500  sbtr  2516  2eumo  2637  abbii  2798  spcimgf  3503  spcgf  3541  euxfr2w  3674  euxfr2  3676  noel  4287  axsepgfromrep  5234  axnulALT  5244  csbex  5251  dtrucor  5311  eusv2nf  5335  axprlem3  5365  axprlem3OLD  5368  ssopab2i  5493  iotabii  6472  opabiotafun  6908  eufnfv  7169  snnex  7697  pwnex  7698  setinds  9645  tz9.13  9690  unir1  9712  axac2  10363  axpowndlem3  10496  uzrdgfni  13871  uvtx01vtx  29382  setinds2regs  35136  unir1regs  35138  hbng  35857  bj-axd2d  36644  bj-exalimsi  36686  bj-hbsb3  36840  bj-nfs1  36843  sbn1ALT  36909  bj-issetw  36927  bj-abf  36960  bj-vtoclf  36966  bj-snsetex  37014  ax4fromc4  38999  ax10fromc7  39000  ax6fromc10  39001  equid1  39004  sn-axprlem3  42316  setindtrs  43123  frege97  44058  frege109  44070  pm11.11  44472  sbeqal1i  44497  axc5c4c711toc7  44502  axc5c4c711to11  44503  iotaequ  44527  mof0  48943  setrec2lem2  49800  vsetrec  49809