Theorem mpg 1792

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

Syntax hints:   → wi 4  ∀wal 1532

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

This theorem is referenced by:  nfth  1796  nfnth  1797  alimi  1806  al2imi  1810  albii  1814  eximi  1830  exbii  1843  nfbii  1847  chvarvv  1995  sbtALT  2065  sbn1  2098  nf5i  2135  chvarfv  2226  hbn  2284  chvar  2389  equsb1  2485  equsb2  2486  nfsb4  2494  sbtr  2510  2eumo  2633  abbii  2797  vtoclfOLD  3548  spcimgf  3574  spcgf  3576  euxfr2w  3713  euxfr2  3715  noel  4326  axsepgfromrep  5291  axnulALT  5298  csbex  5305  dtrucor  5365  eusv2nf  5389  axprlem3  5419  ssopab2i  5546  iotabii  6527  opabiotafun  6973  eufnfv  7235  snnex  7754  pwnex  7755  tz9.13  9806  unir1  9828  axac2  10481  axpowndlem3  10614  uzrdgfni  13947  uvtx01vtx  29197  setinds  35310  hbng  35340  bj-axd2d  36006  bj-exalimsi  36047  bj-hbsb3  36202  bj-nfs1  36205  sbn1ALT  36271  bj-issetw  36289  bj-abf  36323  bj-vtoclf  36329  bj-snsetex  36378  ax4fromc4  38303  ax10fromc7  38304  ax6fromc10  38305  equid1  38308  sn-axprlem3  41625  setindtrs  42368  frege97  43313  frege109  43325  pm11.11  43734  sbeqal1i  43759  axc5c4c711toc7  43764  axc5c4c711to11  43765  iotaequ  43789  mof0  47813  setrec2lem2  48048  vsetrec  48057