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  3717  euxfr2  3719  noel  4331  axsepgfromrep  5298  axnulALT  5305  csbex  5312  dtrucor  5370  eusv2nf  5394  axprlem3  5424  ssopab2i  5551  iotabii  6529  opabiotafun  6973  eufnfv  7231  snnex  7745  pwnex  7746  tz9.13  9786  unir1  9808  axac2  10461  axpowndlem3  10594  uzrdgfni  13923  uvtx01vtx  28654  setinds  34750  hbng  34780  bj-axd2d  35471  bj-exalimsi  35512  bj-hbsb3  35667  bj-nfs1  35670  sbn1ALT  35737  bj-issetw  35755  bj-abf  35789  bj-vtoclf  35795  bj-snsetex  35844  ax4fromc4  37764  ax10fromc7  37765  ax6fromc10  37766  equid1  37769  sn-axprlem3  41034  setindtrs  41764  frege97  42711  frege109  42723  pm11.11  43133  sbeqal1i  43158  axc5c4c711toc7  43163  axc5c4c711to11  43164  iotaequ  43188  mof0  47504  setrec2lem2  47739  vsetrec  47748