Theorem mpg 1791

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

Syntax hints:   → wi 4  ∀wal 1531

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

This theorem is referenced by:  nfth  1795  nfnth  1796  alimi  1805  al2imi  1809  albii  1813  eximi  1829  exbii  1842  nfbii  1846  chvarvv  1994  sbtALT  2064  sbn1  2097  nf5i  2134  chvarfv  2228  hbn  2284  chvar  2388  equsb1  2484  equsb2  2485  nfsb4  2493  sbtr  2509  2eumo  2630  abbii  2795  vtoclfOLD  3544  spcimgf  3574  spcgf  3576  euxfr2w  3713  euxfr2  3715  noel  4331  axsepgfromrep  5297  axnulALT  5304  csbex  5311  dtrucor  5370  eusv2nf  5394  axprlem3  5424  ssopab2i  5551  iotabii  6532  opabiotafun  6976  eufnfv  7239  snnex  7759  pwnex  7760  tz9.13  9814  unir1  9836  axac2  10489  axpowndlem3  10622  uzrdgfni  13955  uvtx01vtx  29266  setinds  35444  hbng  35474  bj-axd2d  36140  bj-exalimsi  36181  bj-hbsb3  36336  bj-nfs1  36339  sbn1ALT  36405  bj-issetw  36423  bj-abf  36457  bj-vtoclf  36463  bj-snsetex  36512  ax4fromc4  38435  ax10fromc7  38436  ax6fromc10  38437  equid1  38440  sn-axprlem3  41774  setindtrs  42511  frege97  43455  frege109  43467  pm11.11  43876  sbeqal1i  43901  axc5c4c711toc7  43906  axc5c4c711to11  43907  iotaequ  43931  mof0  48002  setrec2lem2  48237  vsetrec  48246