Theorem mpg 1797

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

Syntax hints:   → wi 4  ∀wal 1534

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

This theorem is referenced by:  nfth  1801  nfnth  1802  alimi  1811  al2imi  1815  albii  1819  eximi  1834  exbii  1847  nfbii  1851  chvarvv  2004  sbtALT  2073  equsb1vOLD  2112  nf5i  2149  chvarfv  2241  hbn  2302  chvar  2412  equsb1  2529  equsb2  2530  nfsb4  2539  sbtr  2557  equsb1ALT  2600  nfsb4ALT  2604  moimiOLD  2627  mobiiOLD  2631  eubiiOLD  2670  2eumo  2726  abbii  2889  vtoclf  3561  vtocl2OLD  3565  spcimgf  3591  spcgf  3593  euxfr2w  3714  euxfr2  3716  axsepgfromrep  5204  axnulALT  5211  csbex  5218  dtrucor  5275  eusv2nf  5299  axprlem3  5329  ssopab2i  5440  iotabii  6343  opabiotafun  6747  eufnfv  6994  snnex  7483  pwnex  7484  tz9.13  9223  unir1  9245  axac2  9891  axpowndlem3  10024  uzrdgfni  13329  uvtx01vtx  27182  setinds  33027  hbng  33057  bj-axd2d  33931  bj-exalimsi  33972  bj-hbsb3  34115  bj-nfs1  34118  bj-issetw  34194  bj-abf  34229  bj-vtoclf  34235  bj-snsetex  34279  ax4fromc4  36034  ax10fromc7  36035  ax6fromc10  36036  equid1  36039  sn-axprlem3  39115  setindtrs  39628  frege97  40312  frege109  40324  pm11.11  40712  sbeqal1i  40737  axc5c4c711toc7  40742  axc5c4c711to11  40743  iotaequ  40767  setrec2lem2  44804  vsetrec  44812