Theorem mpg 1865

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

Syntax hints:   → wi 4  ∀wal 1622

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

This theorem is referenced by:  nfth  1868  nfnth  1869  alimi  1880  al2imi  1884  albii  1888  eximi  1903  exbii  1915  nfbii  1919  exanOLD  1930  spfwOLD  2109  nf5i  2165  hbn  2285  chvar  2399  chvarv  2400  equsb1  2497  equsb2  2498  nfsb4  2519  sbt  2548  sbtr  2550  moimi  2650  2eumo  2675  vtoclf  3390  vtocl  3391  vtocl2  3393  vtocl3  3394  spcimgf  3418  spcgf  3420  euxfr2  3524  axsep  4924  axnulALT  4931  csbex  4937  eusv2nf  5005  dtrucor  5041  ssopab2i  5145  iotabii  6026  opabiotafun  6413  eufnfv  6646  snnex  7123  pwnex  7125  tz9.13  8819  unir1  8841  axac2  9472  axpowndlem3  9605  uzrdgfni  12943  uvtx01vtx  26492  uvtxa01vtx0OLD  26494  setinds  31980  hbng  32011  bj-axd2d  32875  bj-exalimsi  32912  bj-ssbimi  32921  bj-ssbbii  32922  bj-hbsb3  33011  bj-nfs1  33014  bj-chvarv  33023  bj-chvarvv  33024  bj-equsb1v  33060  bj-sbtv  33064  bj-axsep  33091  bj-dtrucor  33098  bj-vexw  33153  bj-vexwv  33155  bj-issetw  33158  bj-abf  33201  bj-vtoclf  33206  bj-snsetex  33249  ax4fromc4  34675  ax10fromc7  34676  ax6fromc10  34677  equid1  34680  setindtrs  38086  frege97  38748  frege109  38760  pm11.11  39067  sbeqal1i  39093  axc5c4c711toc7  39099  axc5c4c711to11  39100  iotaequ  39124  setrec2lem2  42943  vsetrec  42951