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  3549  spcimgf  3580  spcgf  3582  euxfr2w  3716  euxfr2  3718  noel  4330  axsepgfromrep  5297  axnulALT  5304  csbex  5311  dtrucor  5369  eusv2nf  5393  axprlem3  5423  ssopab2i  5550  iotabii  6526  opabiotafun  6970  eufnfv  7228  snnex  7742  pwnex  7743  tz9.13  9783  unir1  9805  axac2  10458  axpowndlem3  10591  uzrdgfni  13920  uvtx01vtx  28644  setinds  34739  hbng  34769  bj-axd2d  35460  bj-exalimsi  35501  bj-hbsb3  35656  bj-nfs1  35659  sbn1ALT  35726  bj-issetw  35744  bj-abf  35778  bj-vtoclf  35784  bj-snsetex  35833  ax4fromc4  37753  ax10fromc7  37754  ax6fromc10  37755  equid1  37758  sn-axprlem3  41031  setindtrs  41750  frege97  42697  frege109  42709  pm11.11  43119  sbeqal1i  43144  axc5c4c711toc7  43149  axc5c4c711to11  43150  iotaequ  43174  mof0  47458  setrec2lem2  47693  vsetrec  47702