Theorem mpg 1797

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

Syntax hints:   → wi 4  ∀wal 1538

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

This theorem is referenced by:  nfth  1801  nfnth  1802  alimi  1811  al2imi  1815  albii  1819  eximi  1835  exbii  1848  nfbii  1852  chvarvv  1998  sbtALT  2069  sbn1  2107  nf5i  2146  chvarfv  2240  hbn  2295  chvar  2400  equsb1  2496  equsb2  2497  nfsb4  2505  sbtr  2521  2eumo  2642  abbii  2809  spcimgf  3550  vtoclfOLD  3565  spcgf  3591  euxfr2w  3726  euxfr2  3728  noel  4338  axsepgfromrep  5294  axnulALT  5304  csbex  5311  dtrucor  5371  eusv2nf  5395  axprlem3  5425  axprlem3OLD  5428  ssopab2i  5555  iotabii  6546  opabiotafun  6989  eufnfv  7249  snnex  7778  pwnex  7779  tz9.13  9831  unir1  9853  axac2  10506  axpowndlem3  10639  uzrdgfni  13999  uvtx01vtx  29414  setinds  35779  hbng  35809  bj-axd2d  36594  bj-exalimsi  36636  bj-hbsb3  36790  bj-nfs1  36793  sbn1ALT  36859  bj-issetw  36877  bj-abf  36910  bj-vtoclf  36916  bj-snsetex  36964  ax4fromc4  38895  ax10fromc7  38896  ax6fromc10  38897  equid1  38900  sn-axprlem3  42256  setindtrs  43037  frege97  43973  frege109  43985  pm11.11  44393  sbeqal1i  44418  axc5c4c711toc7  44423  axc5c4c711to11  44424  iotaequ  44448  mof0  48747  setrec2lem2  49213  vsetrec  49222