Theorem mpg 1818

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

Syntax hints:   → wi 4  ∀wal 1559

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

This theorem is referenced by:  nfth  1822  nfnth  1823  alimi  1832  al2imi  1836  albii  1840  eximi  1856  exbii  1869  nfbii  1873  chvarvv  2010  sbtALT  2101  sbn1  2142  nf5i  2181  chvarfv  2276  hbn  2330  chvar  2427  equsb1  2523  equsb2  2524  nfsb4  2532  sbtr  2548  moimi  2573  mobii  2576  eubii  2613  2eumo  2670  abbii  2830  spcimgf  3519  spcgf  3551  euxfr2w  3684  euxfr2  3686  noel  4291  axsepgfromrep  5245  axnulALT  5255  csbex  5262  dtrucor  5329  eusv2nf  5353  axprlem3  5383  axprlem3OLD  5387  ssopab2i  5522  iotabii  6506  opabiotafun  6947  eufnfv  7213  snnex  7741  pwnex  7742  setinds  9702  tz9.13  9747  unir1  9769  axac2  10434  axpowndlem3  10568  uzrdgfni  13981  uvtx01vtx  29605  axnulALT2  35379  setinds2regs  35431  unir1regs  35435  hbng  36161  bj-axd2d  37041  bj-exalimsi  37096  bj-hbal  37161  bj-hbsb3  37279  bj-nfs1  37282  sbn1ALT  37348  bj-issetw  37366  bj-abf  37399  bj-vtoclf  37405  bj-snsetex  37453  ax4fromc4  39523  ax10fromc7  39524  ax6fromc10  39525  equid1  39528  sn-axprlem3  42842  setindtrs  43607  frege97  44541  frege109  44553  pm11.11  44941  sbeqal1i  44966  axc5c4c711toc7  44971  axc5c4c711to11  44972  iotaequ  44996  mof0  49450  setrec2lem2  50306  vsetrec  50315