Theorem mpg 1340

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

Syntax hints:   → wi 4  ∀wal 1241

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

This theorem is referenced by:  alimi  1344  albii  1359  a5i  1435  eximi  1491  exbii  1496  19.9h  1534  hbn  1544  chvar  1640  equsb1  1668  equsb2  1669  chvarv  1812  moimi  1965  2eumo  1988  vtoclf  2607  vtocl2  2609  vtocl3  2610  spcimgf  2633  spcimegf  2634  spcgf  2635  spcegf  2636  mosub  2719  csbexa  3886  nalset  3887  ssopab2i  4014  eusv2nf  4188  iotabii  4889  fvmptss2  5247  eufnfv  5389  riotaexg  5472  xpcomco  6300  bj-ex  9902  ch2var  9907  bj-vtoclgf  9915  elabgf1  9918  bj-rspg  9926  bdsepnf  10008  bj-nalset  10015  setindf  10091  strcollnf  10110