Theorem mpg 1497

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

Syntax hints:   → wi 4  ∀wal 1393

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

This theorem is referenced by:  alimi  1501  albii  1516  a5i  1589  nfal  1622  eximi  1646  exbii  1651  19.9h  1689  hbn  1700  chvarfv  1746  chvar  1803  equsb1  1831  equsb2  1832  chvarvv  1955  chvarv  1988  moimi  2143  2eumo  2166  vtoclf  2854  vtocl2  2856  vtocl3  2857  spcimgf  2883  spcimegf  2884  spcgf  2885  spcegf  2886  mosub  2981  csbexa  4213  nalset  4214  ssopab2i  4367  pwnex  4541  eusv2nf  4548  iotabii  5305  fvmptss2  5714  eufnfv  5877  riotaexg  5967  xpcomco  6998  bj-ex  16235  ch2var  16240  bj-vtoclgf  16249  elabgf1  16252  bj-rspg  16260  sumdc2  16272  bdsepnf  16360  bj-nalset  16367  setindf  16438  strcollnf  16457