Theorem mpg 1794

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

Syntax hints:   → wi 4  ∀wal 1535

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

This theorem is referenced by:  nfth  1798  nfnth  1799  alimi  1808  al2imi  1812  albii  1816  eximi  1832  exbii  1845  nfbii  1849  chvarvv  1996  sbtALT  2067  sbn1  2105  nf5i  2144  chvarfv  2238  hbn  2294  chvar  2398  equsb1  2494  equsb2  2495  nfsb4  2503  sbtr  2519  2eumo  2640  abbii  2807  spcimgf  3550  vtoclfOLD  3565  spcgf  3591  euxfr2w  3729  euxfr2  3731  noel  4344  axsepgfromrep  5300  axnulALT  5310  csbex  5317  dtrucor  5377  eusv2nf  5401  axprlem3  5431  axprlem3OLD  5434  ssopab2i  5560  iotabii  6548  opabiotafun  6989  eufnfv  7249  snnex  7777  pwnex  7778  tz9.13  9829  unir1  9851  axac2  10504  axpowndlem3  10637  uzrdgfni  13996  uvtx01vtx  29429  setinds  35760  hbng  35790  bj-axd2d  36576  bj-exalimsi  36618  bj-hbsb3  36772  bj-nfs1  36775  sbn1ALT  36841  bj-issetw  36859  bj-abf  36892  bj-vtoclf  36898  bj-snsetex  36946  ax4fromc4  38876  ax10fromc7  38877  ax6fromc10  38878  equid1  38881  sn-axprlem3  42235  setindtrs  43014  frege97  43950  frege109  43962  pm11.11  44370  sbeqal1i  44395  axc5c4c711toc7  44400  axc5c4c711to11  44401  iotaequ  44425  mof0  48668  setrec2lem2  48925  vsetrec  48934