Theorem mpg 1830

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568

This proof depends on axioms:  ax-mp 5  ax-gen 1828

This theorem is used by:  nfth  1834  nfnth  1835  alimi  1844  al2imi  1848  albii  1852  eximi  1868  exbii  1881  nfbii  1885  chvarvv  2022  sbtALT  2106  sbn1  2144  nf5i  2183  chvarfv  2278  hbn  2330  chvar  2426  equsb1  2522  equsb2  2523  nfsb4  2531  sbtr  2547  moimi  2572  mobii  2575  eubii  2612  2eumo  2669  abbii  2829  spcimgf  3516  spcgf  3548  euxfr2w  3681  euxfr2  3683  noel  4287  axsepgfromrep  5253  axnulALT  5265  csbex  5272  dtrucor  5340  eusv2nf  5364  axprlem3  5394  axprlem3OLD  5398  ssopab2i  5533  iotabii  6522  opabiotafun  6962  eufnfv  7231  snnex  7760  pwnex  7761  setinds  9731  tz9.13  9776  unir1  9798  axac2  10471  axpowndlem3  10611  uzrdgfni  14024  uvtx01vtx  29843  axnulALT2  35577  setinds2regs  35644  unir1regs  35648  hbng  36372  bj-axd2d  37281  bj-exalimsi  37336  bj-hbal  37401  bj-hbsb3  37519  bj-nfs1  37522  sbn1ALT  37588  bj-issetw  37606  bj-abf  37639  bj-vtoclf  37645  bj-snsetex  37694  ax4fromc4  39754  ax10fromc7  39755  ax6fromc10  39756  equid1  39759  sn-axprlem3  43075  setindtrs  43853  frege97  44787  frege109  44799  pm11.11  45185  sbeqal1i  45210  axc5c4c711toc7  45215  axc5c4c711to11  45216  iotaequ  45240  mof0  49753  setrec2lem2  50607  vsetrec  50616