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  2071  sbn1  2109  nf5i  2148  chvarfv  2242  hbn  2296  chvar  2394  equsb1  2490  equsb2  2491  nfsb4  2499  sbtr  2515  2eumo  2636  abbii  2797  spcimgf  3503  vtoclfOLD  3518  spcgf  3544  euxfr2w  3677  euxfr2  3679  noel  4286  axsepgfromrep  5230  axnulALT  5240  csbex  5247  dtrucor  5307  eusv2nf  5331  axprlem3  5361  axprlem3OLD  5364  ssopab2i  5488  iotabii  6462  opabiotafun  6897  eufnfv  7158  snnex  7686  pwnex  7687  tz9.13  9676  unir1  9698  axac2  10349  axpowndlem3  10482  uzrdgfni  13857  uvtx01vtx  29368  setinds2regs  35101  unir1regs  35103  setinds  35791  hbng  35821  bj-axd2d  36606  bj-exalimsi  36648  bj-hbsb3  36802  bj-nfs1  36805  sbn1ALT  36871  bj-issetw  36889  bj-abf  36922  bj-vtoclf  36928  bj-snsetex  36976  ax4fromc4  38912  ax10fromc7  38913  ax6fromc10  38914  equid1  38917  sn-axprlem3  42229  setindtrs  43037  frege97  43972  frege109  43984  pm11.11  44386  sbeqal1i  44411  axc5c4c711toc7  44416  axc5c4c711to11  44417  iotaequ  44441  mof0  48848  setrec2lem2  49705  vsetrec  49714