Theorem mpg 1548

Description: Modus ponens combined with generalization. (Contributed by NM, 24-May-1994.)

Hypotheses

Ref	Expression
mpg.1	⊢ (∀xφ → ψ)
mpg.2	⊢ φ

Assertion

Ref	Expression
mpg	⊢ ψ

Proof of Theorem mpg

Step	Hyp	Ref	Expression
1		mpg.2	. . 3 ⊢ φ
2	1	ax-gen 1546	. 2 ⊢ ∀xφ
3		mpg.1	. 2 ⊢ (∀xφ → ψ)
4	2, 3	ax-mp 5	1 ⊢ ψ

Syntax hints:   → wi 4  ∀wal 1540

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

This theorem is referenced by:  alimi  1559  albii  1566  eximi  1576  exbii  1582  spfw  1691  spw  1694  hbn  1776  19.9hOLD  1781  cbv3  1982  cbv3h  1983  chvar  1986  chvarv  2013  equsb1  2034  equsb2  2035  nfsb4  2081  ax5  2146  ax6  2147  ax9from9o  2148  equid1  2158  moimi  2251  2eumo  2277  vtoclf  2909  vtocl2  2911  vtocl3  2912  spcimgf  2933  spcgf  2935  euxfr2  3022  csbex  3148  iotabii  4362  ssopab2i  4715