Theorem mpg 1807

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

Syntax hints:   → wi 4  ∀wal 1548

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

This theorem is referenced by:  nfth  1811  nfnth  1812  alimi  1821  al2imi  1825  albii  1829  eximi  1845  exbii  1858  nfbii  1862  chvarvv  1999  sbtALT  2090  sbn1  2131  nf5i  2170  chvarfv  2265  hbn  2319  chvar  2416  equsb1  2512  equsb2  2513  nfsb4  2521  sbtr  2537  moimi  2562  mobii  2565  eubii  2602  2eumo  2659  abbii  2819  spcimgf  3508  spcgf  3541  euxfr2w  3673  euxfr2  3675  noel  4281  axsepgfromrep  5234  axnulALT  5244  csbex  5251  dtrucor  5318  eusv2nf  5342  axprlem3  5372  axprlem3OLD  5376  ssopab2i  5510  iotabii  6491  opabiotafun  6932  eufnfv  7198  snnex  7726  pwnex  7727  setinds  9690  tz9.13  9735  unir1  9757  axac2  10409  axpowndlem3  10543  uzrdgfni  13957  uvtx01vtx  29533  axnulALT2  35324  setinds2regs  35372  unir1regs  35376  hbng  36094  bj-axd2d  36974  bj-exalimsi  37029  bj-hbal  37094  bj-hbsb3  37212  bj-nfs1  37215  sbn1ALT  37281  bj-issetw  37299  bj-abf  37332  bj-vtoclf  37338  bj-snsetex  37386  ax4fromc4  39456  ax10fromc7  39457  ax6fromc10  39458  equid1  39461  sn-axprlem3  42775  setindtrs  43540  frege97  44474  frege109  44486  pm11.11  44888  sbeqal1i  44913  axc5c4c711toc7  44918  axc5c4c711to11  44919  iotaequ  44943  mof0  49397  setrec2lem2  50253  vsetrec  50262