Theorem mpg 1444

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

Syntax hints:   → wi 4  ∀wal 1346

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

This theorem is referenced by:  alimi  1448  albii  1463  a5i  1536  nfal  1569  eximi  1593  exbii  1598  19.9h  1636  hbn  1647  chvarfv  1693  chvar  1750  equsb1  1778  equsb2  1779  chvarvv  1901  chvarv  1930  moimi  2084  2eumo  2107  vtoclf  2783  vtocl2  2785  vtocl3  2786  spcimgf  2810  spcimegf  2811  spcgf  2812  spcegf  2813  mosub  2908  csbexa  4118  nalset  4119  ssopab2i  4262  pwnex  4434  eusv2nf  4441  iotabii  5182  fvmptss2  5571  eufnfv  5726  riotaexg  5813  xpcomco  6804  bj-ex  13797  ch2var  13802  bj-vtoclgf  13811  elabgf1  13814  bj-rspg  13822  sumdc2  13834  bdsepnf  13923  bj-nalset  13930  setindf  14001  strcollnf  14020