Theorem mpg 1893

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

Syntax hints:   → wi 4  ∀wal 1651

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

This theorem is referenced by:  nfth  1897  nfnth  1898  alimi  1907  al2imi  1911  albii  1915  eximi  1930  exbii  1944  nfbii  1948  nf5i  2190  equsb1v  2296  hbn  2319  chvar  2402  equsb1  2485  equsb2  2486  nfsb4  2507  sbt  2537  sbtr  2539  mobii  2594  eubii  2625  moimi  2674  2eumo  2701  vtoclf  3445  vtocl  3446  vtocl2  3448  vtocl3  3449  spcimgf  3474  spcgf  3476  euxfr2  3587  axsep  4974  axnulALT  4981  csbex  4988  dtrucor  5041  eusv2nf  5065  ssopab2i  5199  iotabii  6086  opabiotafun  6484  eufnfv  6720  snnex  7200  pwnex  7201  tz9.13  8904  unir1  8926  axac2  9576  axpowndlem3  9709  uzrdgfni  13012  uvtx01vtx  26644  uvtxa01vtx0OLD  26646  setinds  32195  hbng  32226  bj-axd2d  33082  bj-exalimsi  33119  bj-ssbimi  33130  bj-ssbbii  33131  bj-hbsb3  33218  bj-nfs1  33221  bj-chvarv  33230  bj-chvarvv  33231  bj-sbtv  33264  bj-axsep  33289  bj-dtrucor  33296  bj-vexw  33345  bj-vexwv  33347  bj-issetw  33351  bj-abf  33394  bj-vtoclf  33400  bj-snsetex  33443  ax4fromc4  34915  ax10fromc7  34916  ax6fromc10  34917  equid1  34920  setindtrs  38377  frege97  39036  frege109  39048  pm11.11  39355  sbeqal1i  39381  axc5c4c711toc7  39386  axc5c4c711to11  39387  iotaequ  39411  setrec2lem2  43240  vsetrec  43248