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  2855  vtocl2  2857  vtocl3  2858  spcimgf  2884  spcimegf  2885  spcgf  2886  spcegf  2887  mosub  2982  csbexa  4216  nalset  4217  ssopab2i  4370  pwnex  4544  eusv2nf  4551  iotabii  5308  fvmptss2  5717  eufnfv  5880  riotaexg  5970  xpcomco  7005  bj-ex  16308  ch2var  16313  bj-vtoclgf  16322  elabgf1  16325  bj-rspg  16333  sumdc2  16345  bdsepnf  16433  bj-nalset  16440  setindf  16511  strcollnf  16530