Theorem mpg 1380

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

Syntax hints:   → wi 4  ∀wal 1282

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

This theorem is referenced by:  alimi  1384  albii  1399  a5i  1475  eximi  1531  exbii  1536  19.9h  1574  hbn  1584  chvar  1680  equsb1  1708  equsb2  1709  chvarv  1853  moimi  2006  2eumo  2029  vtoclf  2652  vtocl2  2654  vtocl3  2655  spcimgf  2678  spcimegf  2679  spcgf  2680  spcegf  2681  mosub  2770  csbexa  3907  nalset  3908  ssopab2i  4032  eusv2nf  4206  iotabii  4909  fvmptss2  5268  eufnfv  5410  riotaexg  5492  xpcomco  6323  bj-ex  10573  ch2var  10578  bj-vtoclgf  10586  elabgf1  10589  bj-rspg  10597  bdsepnf  10679  bj-nalset  10686  setindf  10761  strcollnf  10780