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  4366  pwnex  4540  eusv2nf  4547  iotabii  5302  fvmptss2  5711  eufnfv  5874  riotaexg  5964  xpcomco  6993  bj-ex  16150  ch2var  16155  bj-vtoclgf  16164  elabgf1  16167  bj-rspg  16175  sumdc2  16187  bdsepnf  16275  bj-nalset  16282  setindf  16353  strcollnf  16372