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  2024  sbtALT  2108  sbn1  2146  nf5i  2186  chvarfv  2280  hbn  2332  chvar  2427  equsb1  2523  equsb2  2524  nfsb4  2532  sbtr  2548  moimi  2573  mobii  2576  eubii  2613  2eumo  2670  abbii  2830  spcimgf  3517  spcgf  3549  euxfr2w  3681  euxfr2  3683  noelOLD  4287  axsepgfromrep  5250  axnulALT  5261  csbex  5268  dtrucor  5337  eusv2nf  5361  axprlem3  5391  ssopab2i  5529  iotabii  6542  opabiotafun  6988  eufnfv  7258  snnex  7796  pwnex  7797  setinds  9777  tz9.13  9825  unir1  9848  setrec2lem2  10003  axac2  10571  axpowndlem3  10711  uzrdgfni  14128  uvtx01vtx  30008  axnulALT2  35784  setinds2regs  35899  unir1regs  35903  hbng  36748  bj-axd2d  37641  bj-exalimsi  37696  bj-hbal  37761  bj-hbsb3  37879  bj-nfs1  37882  sbn1ALT  37948  bj-issetw  37966  bj-abf  37999  bj-vtoclf  38005  bj-snsetex  38054  ax4fromc4  40143  ax10fromc7  40144  ax6fromc10  40145  equid1  40148  sn-axprlem3  43465  setindtrs  44225  frege97  45152  frege109  45164  pm11.11  45550  sbeqal1i  45575  axc5c4c711toc7  45580  axc5c4c711to11  45581  iotaequ  45604  mof0  50154  vsetrec  51076