Theorem mpg 1715

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

Syntax hints:   → wi 4  ∀wal 1473

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

This theorem is referenced by:  nfth  1718  nfnth  1719  alimi  1730  al2imi  1733  albii  1737  eximi  1752  exbii  1764  exanOLD  1776  spfwOLD  1953  nf5i  2011  hbn  2131  chvar  2250  chvarv  2251  equsb1  2356  equsb2  2357  nfsb4  2378  sbt  2407  sbtr  2409  moimi  2508  2eumo  2533  vtoclf  3231  vtocl  3232  vtocl2  3234  vtocl3  3235  spcimgf  3259  spcgf  3261  euxfr2  3358  axsep  4708  axnulALT  4715  csbex  4721  eusv2nf  4790  dtrucor  4827  ssopab2i  4928  iotabii  5790  opabiotafun  6169  eufnfv  6395  tz9.13  8537  unir1  8559  axac2  9171  axpowndlem3  9300  uzrdgfni  12619  setinds  30927  hbng  30958  bj-axd2d  31750  bj-nfth  31772  bj-nfnth  31774  bj-nfxfr  31794  bj-ssbimi  31812  bj-ssbbii  31813  bj-hbsb3  31900  bj-nfs1  31903  bj-chvarv  31912  bj-chvarvv  31913  bj-equsb1v  31950  bj-sbtv  31954  bj-axsep  31981  bj-dtrucor  31988  bj-vexw  32049  bj-vexwv  32051  bj-issetw  32054  bj-abf  32095  bj-vtoclf  32100  bj-snsetex  32144  bj-pwnex  32246  ax4fromc4  33197  ax10fromc7  33198  ax6fromc10  33199  equid1  33202  setindtrs  36610  frege97  37274  frege109  37286  pm11.11  37595  sbeqal1i  37621  axc5c4c711toc7  37627  axc5c4c711to11  37628  iotaequ  37652  uvtxa01vtx0  40623  setrec2lem2  42240  vsetrec  42245