Theorem mpg 1826

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

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

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

This theorem is used by:  nfth  1830  nfnth  1831  alimi  1840  al2imi  1844  albii  1848  eximi  1864  exbii  1877  nfbii  1881  chvarvv  2018  sbtALT  2102  sbn1  2141  nf5i  2180  chvarfv  2275  hbn  2329  chvar  2426  equsb1  2522  equsb2  2523  nfsb4  2531  sbtr  2547  moimi  2572  mobii  2575  eubii  2612  2eumo  2669  abbii  2829  spcimgf  3517  spcgf  3549  euxfr2w  3682  euxfr2  3684  noel  4290  axsepgfromrep  5254  axnulALT  5266  csbex  5273  dtrucor  5341  eusv2nf  5365  axprlem3  5395  axprlem3OLD  5399  ssopab2i  5534  iotabii  6521  opabiotafun  6961  eufnfv  7227  snnex  7755  pwnex  7756  setinds  9716  tz9.13  9761  unir1  9783  axac2  10456  axpowndlem3  10590  uzrdgfni  14001  uvtx01vtx  29758  axnulALT2  35480  setinds2regs  35552  unir1regs  35556  hbng  36306  bj-axd2d  37214  bj-exalimsi  37269  bj-hbal  37334  bj-hbsb3  37452  bj-nfs1  37455  sbn1ALT  37521  bj-issetw  37539  bj-abf  37572  bj-vtoclf  37578  bj-snsetex  37627  ax4fromc4  39696  ax10fromc7  39697  ax6fromc10  39698  equid1  39701  sn-axprlem3  43017  setindtrs  43780  frege97  44714  frege109  44726  pm11.11  45112  sbeqal1i  45137  axc5c4c711toc7  45142  axc5c4c711to11  45143  iotaequ  45167  mof0  49644  setrec2lem2  50500  vsetrec  50509