Theorem mpg 1796

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

Syntax hints:   → wi 4  ∀wal 1537

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

This theorem is referenced by:  nfth  1800  nfnth  1801  alimi  1810  al2imi  1814  albii  1818  eximi  1834  exbii  1847  nfbii  1851  chvarvv  1997  sbtALT  2068  sbn1  2106  nf5i  2145  chvarfv  2239  hbn  2294  chvar  2398  equsb1  2494  equsb2  2495  nfsb4  2503  sbtr  2519  2eumo  2640  abbii  2801  spcimgf  3533  vtoclfOLD  3548  spcgf  3574  euxfr2w  3708  euxfr2  3710  noel  4318  axsepgfromrep  5274  axnulALT  5284  csbex  5291  dtrucor  5351  eusv2nf  5375  axprlem3  5405  axprlem3OLD  5408  ssopab2i  5535  iotabii  6526  opabiotafun  6969  eufnfv  7231  snnex  7760  pwnex  7761  tz9.13  9813  unir1  9835  axac2  10488  axpowndlem3  10621  uzrdgfni  13981  uvtx01vtx  29343  setinds  35754  hbng  35784  bj-axd2d  36569  bj-exalimsi  36611  bj-hbsb3  36765  bj-nfs1  36768  sbn1ALT  36834  bj-issetw  36852  bj-abf  36885  bj-vtoclf  36891  bj-snsetex  36939  ax4fromc4  38870  ax10fromc7  38871  ax6fromc10  38872  equid1  38875  sn-axprlem3  42231  setindtrs  43015  frege97  43950  frege109  43962  pm11.11  44365  sbeqal1i  44390  axc5c4c711toc7  44395  axc5c4c711to11  44396  iotaequ  44420  mof0  48724  setrec2lem2  49308  vsetrec  49317