Theorem mpg 1439

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

Syntax hints:   → wi 4  ∀wal 1341

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

This theorem is referenced by:  alimi  1443  albii  1458  a5i  1531  nfal  1564  eximi  1588  exbii  1593  19.9h  1631  hbn  1642  chvarfv  1688  chvar  1745  equsb1  1773  equsb2  1774  chvarvv  1896  chvarv  1925  moimi  2079  2eumo  2102  vtoclf  2779  vtocl2  2781  vtocl3  2782  spcimgf  2806  spcimegf  2807  spcgf  2808  spcegf  2809  mosub  2904  csbexa  4111  nalset  4112  ssopab2i  4255  pwnex  4427  eusv2nf  4434  iotabii  5175  fvmptss2  5561  eufnfv  5715  riotaexg  5802  xpcomco  6792  bj-ex  13643  ch2var  13648  bj-vtoclgf  13657  elabgf1  13660  bj-rspg  13668  sumdc2  13680  bdsepnf  13770  bj-nalset  13777  setindf  13848  strcollnf  13867