Theorem mpg 1825

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

Syntax hints:   → wi 4  ∀wal 1566

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

This theorem is referenced by:  nfth  1829  nfnth  1830  alimi  1839  al2imi  1843  albii  1847  eximi  1863  exbii  1876  nfbii  1880  chvarvv  2017  sbtALT  2101  sbn1  2140  nf5i  2179  chvarfv  2274  hbn  2328  chvar  2425  equsb1  2521  equsb2  2522  nfsb4  2530  sbtr  2546  moimi  2571  mobii  2574  eubii  2611  2eumo  2668  abbii  2828  spcimgf  3517  spcgf  3549  euxfr2w  3682  euxfr2  3684  noel  4290  axsepgfromrep  5254  axnulALT  5266  csbex  5273  dtrucor  5342  eusv2nf  5366  axprlem3  5396  axprlem3OLD  5400  ssopab2i  5535  iotabii  6521  opabiotafun  6961  eufnfv  7227  snnex  7756  pwnex  7757  setinds  9717  tz9.13  9762  unir1  9784  axac2  10449  axpowndlem3  10583  uzrdgfni  13993  uvtx01vtx  29713  axnulALT2  35436  setinds2regs  35498  unir1regs  35502  hbng  36252  bj-axd2d  37130  bj-exalimsi  37185  bj-hbal  37250  bj-hbsb3  37368  bj-nfs1  37371  sbn1ALT  37437  bj-issetw  37455  bj-abf  37488  bj-vtoclf  37494  bj-snsetex  37543  ax4fromc4  39614  ax10fromc7  39615  ax6fromc10  39616  equid1  39619  sn-axprlem3  42935  setindtrs  43700  frege97  44634  frege109  44646  pm11.11  45032  sbeqal1i  45057  axc5c4c711toc7  45062  axc5c4c711to11  45063  iotaequ  45087  mof0  49561  setrec2lem2  50417  vsetrec  50426