Theorem mpg 1504

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

Syntax hints:   → wi 4  ∀wal 1400

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

This theorem is referenced by:  alimi  1508  albii  1523  a5i  1596  nfal  1629  eximi  1653  exbii  1658  19.9h  1696  hbnOLD  1706  chvarfv  1752  chvar  1810  equsb1  1838  equsb2  1839  chvarvv  1964  chvarv  1997  moimi  2152  2eumo  2175  vtoclf  2876  vtocl2  2878  vtocl3  2879  spcimgf  2905  spcimegf  2906  spcgf  2907  spcegf  2908  mosub  3004  csbexa  4260  nalset  4261  ssopab2i  4418  pwnex  4593  eusv2nf  4600  iotabii  5359  fvmptss2  5777  eufnfv  5943  riotaexg  6036  xpcomco  7118  bj-ex  16773  ch2var  16778  bj-vtoclgf  16787  elabgf1  16790  bj-rspg  16798  sumdc2  16810  bdsepnf  16897  bj-nalset  16904  setindf  16975  strcollnf  16994