Theorem mpg 1462

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

Syntax hints:   → wi 4  ∀wal 1362

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

This theorem is referenced by:  alimi  1466  albii  1481  a5i  1554  nfal  1587  eximi  1611  exbii  1616  19.9h  1654  hbn  1665  chvarfv  1711  chvar  1768  equsb1  1796  equsb2  1797  chvarvv  1920  chvarv  1949  moimi  2103  2eumo  2126  vtoclf  2805  vtocl2  2807  vtocl3  2808  spcimgf  2832  spcimegf  2833  spcgf  2834  spcegf  2835  mosub  2930  csbexa  4147  nalset  4148  ssopab2i  4295  pwnex  4467  eusv2nf  4474  iotabii  5219  fvmptss2  5611  eufnfv  5767  riotaexg  5855  xpcomco  6851  bj-ex  14967  ch2var  14972  bj-vtoclgf  14981  elabgf1  14984  bj-rspg  14992  sumdc2  15004  bdsepnf  15093  bj-nalset  15100  setindf  15171  strcollnf  15190