Theorem mpg 1381

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

Syntax hints:   → wi 4  ∀wal 1283

This theorem was proved from axioms:  ax-mp 7  ax-gen 1379

This theorem is referenced by:  alimi  1385  albii  1400  a5i  1476  eximi  1532  exbii  1537  19.9h  1575  hbn  1585  chvar  1682  equsb1  1710  equsb2  1711  chvarv  1855  moimi  2008  2eumo  2031  vtoclf  2661  vtocl2  2663  vtocl3  2664  spcimgf  2687  spcimegf  2688  spcgf  2689  spcegf  2690  mosub  2779  csbexa  3927  nalset  3928  ssopab2i  4060  eusv2nf  4234  iotabii  4939  fvmptss2  5299  eufnfv  5441  riotaexg  5523  xpcomco  6391  bj-ex  10833  ch2var  10838  bj-vtoclgf  10846  elabgf1  10849  bj-rspg  10857  sumdc2  10869  bdsepnf  10946  bj-nalset  10953  setindf  11028  strcollnf  11047