Theorem mpg 1800

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 1798	. 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 1798

This theorem is referenced by:  nfth  1804  nfnth  1805  alimi  1814  al2imi  1818  albii  1822  eximi  1838  exbii  1851  nfbii  1855  chvarvv  2003  sbtALT  2073  sbn1  2106  nf5i  2143  chvarfv  2234  hbn  2292  chvar  2395  equsb1  2491  equsb2  2492  nfsb4  2500  sbtr  2516  2eumo  2639  abbii  2803  vtoclfOLD  3548  spcimgf  3579  spcgf  3581  euxfr2w  3715  euxfr2  3717  noel  4329  axsepgfromrep  5296  axnulALT  5303  csbex  5310  dtrucor  5368  eusv2nf  5392  axprlem3  5422  ssopab2i  5549  iotabii  6525  opabiotafun  6968  eufnfv  7226  snnex  7740  pwnex  7741  tz9.13  9782  unir1  9804  axac2  10457  axpowndlem3  10590  uzrdgfni  13919  uvtx01vtx  28634  setinds  34688  hbng  34718  bj-axd2d  35409  bj-exalimsi  35450  bj-hbsb3  35605  bj-nfs1  35608  sbn1ALT  35675  bj-issetw  35693  bj-abf  35727  bj-vtoclf  35733  bj-snsetex  35782  ax4fromc4  37702  ax10fromc7  37703  ax6fromc10  37704  equid1  37707  sn-axprlem3  40982  setindtrs  41697  frege97  42644  frege109  42656  pm11.11  43066  sbeqal1i  43091  axc5c4c711toc7  43096  axc5c4c711to11  43097  iotaequ  43121  mof0  47406  setrec2lem2  47641  vsetrec  47650