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  4292  pwnex  4464  eusv2nf  4471  iotabii  5216  fvmptss2  5608  eufnfv  5764  riotaexg  5852  xpcomco  6845  bj-ex  14918  ch2var  14923  bj-vtoclgf  14932  elabgf1  14935  bj-rspg  14943  sumdc2  14955  bdsepnf  15044  bj-nalset  15051  setindf  15122  strcollnf  15141