Theorem mpg 1829

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567

This proof depends on axioms:  ax-mp 5  ax-gen 1827

This theorem is used by:  nfth  1833  nfnth  1834  alimi  1843  al2imi  1847  albii  1851  eximi  1867  exbii  1880  nfbii  1884  chvarvv  2021  sbtALT  2105  sbn1  2143  nf5i  2182  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  5524  iotabii  6523  opabiotafun  6965  eufnfv  7235  snnex  7772  pwnex  7773  setinds  9750  tz9.13  9798  unir1  9821  setrec2lem2  9976  axac2  10544  axpowndlem3  10684  uzrdgfni  14101  uvtx01vtx  29978  axnulALT2  35754  setinds2regs  35841  unir1regs  35845  hbng  36612  bj-axd2d  37505  bj-exalimsi  37560  bj-hbal  37625  bj-hbsb3  37743  bj-nfs1  37746  sbn1ALT  37812  bj-issetw  37830  bj-abf  37863  bj-vtoclf  37869  bj-snsetex  37918  ax4fromc4  39994  ax10fromc7  39995  ax6fromc10  39996  equid1  39999  sn-axprlem3  43315  setindtrs  44075  frege97  45003  frege109  45015  pm11.11  45401  sbeqal1i  45426  axc5c4c711toc7  45431  axc5c4c711to11  45432  iotaequ  45456  mof0  49991  vsetrec  50839