Theorem mpg 1500

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

Syntax hints:   → wi 4  ∀wal 1396

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

This theorem is referenced by:  alimi  1504  albii  1519  a5i  1592  nfal  1625  eximi  1649  exbii  1654  19.9h  1692  hbnOLD  1702  chvarfv  1748  chvar  1806  equsb1  1834  equsb2  1835  chvarvv  1960  chvarv  1993  moimi  2148  2eumo  2171  vtoclf  2870  vtocl2  2872  vtocl3  2873  spcimgf  2899  spcimegf  2900  spcgf  2901  spcegf  2902  mosub  2998  csbexa  4244  nalset  4245  ssopab2i  4401  pwnex  4575  eusv2nf  4582  iotabii  5341  fvmptss2  5757  eufnfv  5922  riotaexg  6015  xpcomco  7090  bj-ex  16673  ch2var  16678  bj-vtoclgf  16687  elabgf1  16690  bj-rspg  16698  sumdc2  16710  bdsepnf  16797  bj-nalset  16804  setindf  16875  strcollnf  16894