Theorem mpg 1385

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

Syntax hints:   → wi 4  ∀wal 1287

This theorem was proved from axioms:  ax-mp 7  ax-gen 1383

This theorem is referenced by:  alimi  1389  albii  1404  a5i  1480  eximi  1536  exbii  1541  19.9h  1579  hbn  1589  chvar  1687  equsb1  1715  equsb2  1716  chvarv  1860  moimi  2013  2eumo  2036  vtoclf  2672  vtocl2  2674  vtocl3  2675  spcimgf  2699  spcimegf  2700  spcgf  2701  spcegf  2702  mosub  2791  csbexa  3960  nalset  3961  ssopab2i  4095  eusv2nf  4269  iotabii  4989  fvmptss2  5363  eufnfv  5507  riotaexg  5594  xpcomco  6522  bj-ex  11309  ch2var  11314  bj-vtoclgf  11322  elabgf1  11325  bj-rspg  11333  sumdc2  11345  bdsepnf  11425  bj-nalset  11432  setindf  11507  strcollnf  11526