Theorem mpg 1461

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

Syntax hints:   → wi 4  ∀wal 1361

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

This theorem is referenced by:  alimi  1465  albii  1480  a5i  1553  nfal  1586  eximi  1610  exbii  1615  19.9h  1653  hbn  1664  chvarfv  1710  chvar  1767  equsb1  1795  equsb2  1796  chvarvv  1918  chvarv  1947  moimi  2101  2eumo  2124  vtoclf  2802  vtocl2  2804  vtocl3  2805  spcimgf  2829  spcimegf  2830  spcgf  2831  spcegf  2832  mosub  2927  csbexa  4144  nalset  4145  ssopab2i  4289  pwnex  4461  eusv2nf  4468  iotabii  5212  fvmptss2  5604  eufnfv  5760  riotaexg  5848  xpcomco  6840  bj-ex  14810  ch2var  14815  bj-vtoclgf  14824  elabgf1  14827  bj-rspg  14835  sumdc2  14847  bdsepnf  14936  bj-nalset  14943  setindf  15014  strcollnf  15033