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  7129  bj-ex  17007  ch2var  17012  bj-vtoclgf  17021  elabgf1  17024  bj-rspg  17032  sumdc2  17044  bdsepnf  17131  bj-nalset  17138  setindf  17209  strcollnf  17228