Theorem mpg 1801

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

Syntax hints:   → wi 4  ∀wal 1537

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

This theorem is referenced by:  nfth  1805  nfnth  1806  alimi  1815  al2imi  1819  albii  1823  eximi  1838  exbii  1851  nfbii  1855  chvarvv  2003  sbtALT  2073  sbn1  2107  nf5i  2144  chvarfv  2236  hbn  2295  chvar  2395  equsb1  2495  equsb2  2496  nfsb4  2504  sbtr  2520  2eumo  2644  abbii  2809  vtoclf  3487  spcimgf  3518  spcgf  3520  euxfr2w  3650  euxfr2  3652  noel  4261  axsepgfromrep  5216  axnulALT  5223  csbex  5230  dtrucor  5289  eusv2nf  5313  axprlem3  5343  ssopab2i  5456  iotabii  6403  opabiotafun  6831  eufnfv  7087  snnex  7586  pwnex  7587  tz9.13  9480  unir1  9502  axac2  10153  axpowndlem3  10286  uzrdgfni  13606  uvtx01vtx  27667  setinds  33660  hbng  33690  bj-axd2d  34702  bj-exalimsi  34743  bj-hbsb3  34898  bj-nfs1  34901  sbn1ALT  34969  bj-issetw  34987  bj-abf  35021  bj-vtoclf  35027  bj-snsetex  35080  ax4fromc4  36835  ax10fromc7  36836  ax6fromc10  36837  equid1  36840  sn-axprlem3  40114  setindtrs  40763  frege97  41457  frege109  41469  pm11.11  41881  sbeqal1i  41906  axc5c4c711toc7  41911  axc5c4c711to11  41912  iotaequ  41936  mof0  46053  setrec2lem2  46286  vsetrec  46294