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  2276  hbn  2328  chvar  2424  equsb1  2520  equsb2  2521  nfsb4  2529  sbtr  2545  moimi  2570  mobii  2573  eubii  2610  2eumo  2667  abbii  2827  spcimgf  3513  spcgf  3545  euxfr2w  3677  euxfr2  3679  noel  4283  axsepgfromrep  5246  axnulALT  5257  csbex  5264  dtrucor  5332  eusv2nf  5356  axprlem3  5386  ssopab2i  5521  iotabii  6512  opabiotafun  6953  eufnfv  7223  snnex  7755  pwnex  7756  setinds  9728  tz9.13  9773  unir1  9795  setrec2lem2  9947  axac2  10515  axpowndlem3  10655  uzrdgfni  14069  uvtx01vtx  29911  axnulALT2  35645  setinds2regs  35724  unir1regs  35728  hbng  36492  bj-axd2d  37385  bj-exalimsi  37440  bj-hbal  37505  bj-hbsb3  37623  bj-nfs1  37626  sbn1ALT  37692  bj-issetw  37710  bj-abf  37743  bj-vtoclf  37749  bj-snsetex  37798  ax4fromc4  39871  ax10fromc7  39872  ax6fromc10  39873  equid1  39876  sn-axprlem3  43192  setindtrs  43970  frege97  44904  frege109  44916  pm11.11  45302  sbeqal1i  45327  axc5c4c711toc7  45332  axc5c4c711to11  45333  iotaequ  45357  mof0  49870  vsetrec  50718