Theorem mpg 1475

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

Syntax hints:   → wi 4  ∀wal 1371

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

This theorem is referenced by:  alimi  1479  albii  1494  a5i  1567  nfal  1600  eximi  1624  exbii  1629  19.9h  1667  hbn  1678  chvarfv  1724  chvar  1781  equsb1  1809  equsb2  1810  chvarvv  1933  chvarv  1966  moimi  2120  2eumo  2143  vtoclf  2827  vtocl2  2829  vtocl3  2830  spcimgf  2854  spcimegf  2855  spcgf  2856  spcegf  2857  mosub  2952  csbexa  4177  nalset  4178  ssopab2i  4328  pwnex  4500  eusv2nf  4507  iotabii  5260  fvmptss2  5661  eufnfv  5822  riotaexg  5910  xpcomco  6928  bj-ex  15772  ch2var  15777  bj-vtoclgf  15786  elabgf1  15789  bj-rspg  15797  sumdc2  15809  bdsepnf  15898  bj-nalset  15905  setindf  15976  strcollnf  15995