Theorem mpg 1499

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

Syntax hints:   → wi 4  ∀wal 1395

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

This theorem is referenced by:  alimi  1503  albii  1518  a5i  1591  nfal  1624  eximi  1648  exbii  1653  19.9h  1691  hbn  1702  chvarfv  1748  chvar  1805  equsb1  1833  equsb2  1834  chvarvv  1957  chvarv  1990  moimi  2145  2eumo  2168  vtoclf  2857  vtocl2  2859  vtocl3  2860  spcimgf  2886  spcimegf  2887  spcgf  2888  spcegf  2889  mosub  2984  csbexa  4218  nalset  4219  ssopab2i  4372  pwnex  4546  eusv2nf  4553  iotabii  5310  fvmptss2  5721  eufnfv  5885  riotaexg  5975  xpcomco  7010  bj-ex  16379  ch2var  16384  bj-vtoclgf  16393  elabgf1  16396  bj-rspg  16404  sumdc2  16416  bdsepnf  16504  bj-nalset  16511  setindf  16582  strcollnf  16601