Theorem mpg 1800

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 1798	. 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 1798

This theorem is referenced by:  nfth  1804  nfnth  1805  alimi  1814  al2imi  1818  albii  1822  eximi  1837  exbii  1850  nfbii  1854  chvarvv  2002  sbtALT  2072  sbn1  2105  nf5i  2142  chvarfv  2233  hbn  2292  chvar  2395  equsb1  2495  equsb2  2496  nfsb4  2504  sbtr  2520  2eumo  2644  abbii  2808  vtoclf  3497  spcimgf  3528  spcgf  3530  euxfr2w  3655  euxfr2  3657  noel  4264  axsepgfromrep  5221  axnulALT  5228  csbex  5235  dtrucor  5294  eusv2nf  5318  axprlem3  5348  ssopab2i  5463  iotabii  6418  opabiotafun  6849  eufnfv  7105  snnex  7608  pwnex  7609  tz9.13  9549  unir1  9571  axac2  10222  axpowndlem3  10355  uzrdgfni  13678  uvtx01vtx  27764  setinds  33754  hbng  33784  bj-axd2d  34775  bj-exalimsi  34816  bj-hbsb3  34971  bj-nfs1  34974  sbn1ALT  35042  bj-issetw  35060  bj-abf  35094  bj-vtoclf  35100  bj-snsetex  35153  ax4fromc4  36908  ax10fromc7  36909  ax6fromc10  36910  equid1  36913  sn-axprlem3  40186  setindtrs  40847  frege97  41568  frege109  41580  pm11.11  41992  sbeqal1i  42017  axc5c4c711toc7  42022  axc5c4c711to11  42023  iotaequ  42047  mof0  46165  setrec2lem2  46400  vsetrec  46408