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  4262  nalset  4263  ssopab2i  4420  pwnex  4595  eusv2nf  4602  iotabii  5361  fvmptss2  5780  eufnfv  5949  riotaexg  6042  xpcomco  7124  bj-ex  16909  ch2var  16914  bj-vtoclgf  16923  elabgf1  16926  bj-rspg  16934  sumdc2  16946  bdsepnf  17033  bj-nalset  17040  setindf  17111  strcollnf  17130