Theorem mpg 1799

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

Syntax hints:   → wi 4  ∀wal 1536

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

This theorem is referenced by:  nfth  1803  nfnth  1804  alimi  1813  al2imi  1817  albii  1821  eximi  1836  exbii  1849  nfbii  1853  chvarvv  2005  sbtALT  2074  equsb1vOLD  2110  nf5i  2147  chvarfv  2240  hbn  2299  chvar  2402  equsb1  2509  equsb2  2510  nfsb4  2518  sbtr  2535  equsb1ALT  2577  nfsb4ALT  2581  mobiiOLD  2607  eubiiOLD  2646  2eumo  2704  abbii  2863  vtoclf  3506  vtocl2OLD  3510  spcimgf  3536  spcgf  3538  euxfr2w  3659  euxfr2  3661  axsepgfromrep  5165  axnulALT  5172  csbex  5179  dtrucor  5237  eusv2nf  5261  axprlem3  5291  ssopab2i  5402  iotabii  6309  opabiotafun  6719  eufnfv  6969  snnex  7460  pwnex  7461  tz9.13  9204  unir1  9226  axac2  9877  axpowndlem3  10010  uzrdgfni  13321  uvtx01vtx  27187  setinds  33136  hbng  33166  bj-axd2d  34040  bj-exalimsi  34081  bj-hbsb3  34226  bj-nfs1  34229  bj-issetw  34314  bj-abf  34349  bj-vtoclf  34355  bj-snsetex  34399  ax4fromc4  36190  ax10fromc7  36191  ax6fromc10  36192  equid1  36195  sn-axprlem3  39401  setindtrs  39966  frege97  40661  frege109  40673  pm11.11  41078  sbeqal1i  41103  axc5c4c711toc7  41108  axc5c4c711to11  41109  iotaequ  41133  setrec2lem2  45224  vsetrec  45232