Theorem mpg 1795

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

Syntax hints:   → wi 4  ∀wal 1535

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

This theorem is referenced by:  nfth  1799  nfnth  1800  alimi  1809  al2imi  1813  albii  1817  eximi  1833  exbii  1846  nfbii  1850  chvarvv  1998  sbtALT  2069  sbn1  2107  nf5i  2146  chvarfv  2241  hbn  2299  chvar  2403  equsb1  2499  equsb2  2500  nfsb4  2508  sbtr  2524  2eumo  2645  abbii  2812  spcimgf  3562  vtoclfOLD  3577  spcgf  3604  euxfr2w  3742  euxfr2  3744  noel  4360  axsepgfromrep  5315  axnulALT  5322  csbex  5329  dtrucor  5389  eusv2nf  5413  axprlem3  5443  ssopab2i  5569  iotabii  6558  opabiotafun  7002  eufnfv  7266  snnex  7793  pwnex  7794  tz9.13  9860  unir1  9882  axac2  10535  axpowndlem3  10668  uzrdgfni  14009  uvtx01vtx  29432  setinds  35742  hbng  35772  bj-axd2d  36559  bj-exalimsi  36601  bj-hbsb3  36755  bj-nfs1  36758  sbn1ALT  36824  bj-issetw  36842  bj-abf  36875  bj-vtoclf  36881  bj-snsetex  36929  ax4fromc4  38850  ax10fromc7  38851  ax6fromc10  38852  equid1  38855  sn-axprlem3  42210  setindtrs  42982  frege97  43922  frege109  43934  pm11.11  44343  sbeqal1i  44368  axc5c4c711toc7  44373  axc5c4c711to11  44374  iotaequ  44398  mof0  48551  setrec2lem2  48786  vsetrec  48795