Theorem mpg 1799

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

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  nfth  1803  nfnth  1804  alimi  1813  al2imi  1817  albii  1821  eximi  1837  exbii  1850  nfbii  1854  chvarvv  1991  sbtALT  2075  sbn1  2113  nf5i  2152  chvarfv  2248  hbn  2302  chvar  2400  equsb1  2496  equsb2  2497  nfsb4  2505  sbtr  2521  moimi  2546  mobii  2549  eubii  2586  2eumo  2643  abbii  2804  spcimgf  3496  spcgf  3534  euxfr2w  3667  euxfr2  3669  noel  4279  axsepgfromrep  5230  axnulALT  5240  csbex  5247  dtrucor  5314  eusv2nf  5338  axprlem3  5368  axprlem3OLD  5372  ssopab2i  5505  iotabii  6484  opabiotafun  6921  eufnfv  7184  snnex  7712  pwnex  7713  setinds  9670  tz9.13  9715  unir1  9737  axac2  10388  axpowndlem3  10522  uzrdgfni  13920  uvtx01vtx  29466  axnulALT2  35224  setinds2regs  35275  unir1regs  35279  hbng  35988  bj-axd2d  36858  bj-exalimsi  36913  bj-hbal  36978  bj-hbsb3  37096  bj-nfs1  37099  sbn1ALT  37165  bj-issetw  37183  bj-abf  37216  bj-vtoclf  37222  bj-snsetex  37270  ax4fromc4  39340  ax10fromc7  39341  ax6fromc10  39342  equid1  39345  sn-axprlem3  42659  setindtrs  43453  frege97  44387  frege109  44399  pm11.11  44801  sbeqal1i  44826  axc5c4c711toc7  44831  axc5c4c711to11  44832  iotaequ  44856  mof0  49307  setrec2lem2  50163  vsetrec  50172