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  1958  chvarv  1991  moimi  2146  2eumo  2169  vtoclf  2867  vtocl2  2869  vtocl3  2870  spcimgf  2896  spcimegf  2897  spcgf  2898  spcegf  2899  mosub  2994  csbexa  4238  nalset  4239  ssopab2i  4395  pwnex  4569  eusv2nf  4576  iotabii  5335  fvmptss2  5751  eufnfv  5916  riotaexg  6006  xpcomco  7076  bj-ex  16521  ch2var  16526  bj-vtoclgf  16535  elabgf1  16538  bj-rspg  16546  sumdc2  16558  bdsepnf  16645  bj-nalset  16652  setindf  16723  strcollnf  16742