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 ⊢ 𝜓

This proof depends on syntax axioms:   → wi 4  ∀wal 1400

This proof depends on axioms:  ax-mp 5  ax-gen 1502

This theorem is used 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  4264  nalset  4265  ssopab2i  4422  pwnex  4597  eusv2nf  4604  iotabii  5364  fvmptss2  5783  eufnfv  5952  riotaexg  6045  xpcomco  7130  bj-ex  17012  ch2var  17017  bj-vtoclgf  17026  elabgf1  17029  bj-rspg  17037  sumdc2  17049  bdsepnf  17136  bj-nalset  17143  setindf  17214  strcollnf  17233