Theorem mpg 1764

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

Syntax hints:   → wi 4  ∀wal 1521

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

This theorem is referenced by:  nfth  1767  nfnth  1768  alimi  1779  al2imi  1783  albii  1787  eximi  1802  exbii  1814  nfbii  1818  exanOLD  1829  spfwOLD  2008  nf5i  2064  hbn  2184  chvar  2298  chvarv  2299  equsb1  2396  equsb2  2397  nfsb4  2418  sbt  2447  sbtr  2449  moimi  2549  2eumo  2574  vtoclf  3289  vtocl  3290  vtocl2  3292  vtocl3  3293  spcimgf  3317  spcgf  3319  euxfr2  3424  axsep  4813  axnulALT  4820  csbex  4826  eusv2nf  4894  dtrucor  4930  ssopab2i  5032  iotabii  5911  opabiotafun  6298  eufnfv  6531  snnex  7008  pwnex  7010  tz9.13  8692  unir1  8714  axac2  9326  axpowndlem3  9459  uzrdgfni  12797  uvtx01vtx  26346  uvtxa01vtx0OLD  26348  setinds  31807  hbng  31838  bj-axd2d  32702  bj-exalimsi  32739  bj-ssbimi  32748  bj-ssbbii  32749  bj-hbsb3  32838  bj-nfs1  32841  bj-chvarv  32850  bj-chvarvv  32851  bj-equsb1v  32887  bj-sbtv  32891  bj-axsep  32918  bj-dtrucor  32925  bj-vexw  32980  bj-vexwv  32982  bj-issetw  32985  bj-abf  33028  bj-vtoclf  33033  bj-snsetex  33076  ax4fromc4  34498  ax10fromc7  34499  ax6fromc10  34500  equid1  34503  setindtrs  37909  frege97  38571  frege109  38583  pm11.11  38890  sbeqal1i  38916  axc5c4c711toc7  38922  axc5c4c711to11  38923  iotaequ  38947  setrec2lem2  42766  vsetrec  42774