Theorem sps-o 2159

Description: Generalization of antecedent. (Contributed by NM, 5-Aug-1993.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypothesis

Ref	Expression
sps-o.1	⊢ (φ → ψ)

Assertion

Ref	Expression
sps-o	⊢ (∀xφ → ψ)

Proof of Theorem sps-o

Step	Hyp	Ref	Expression
1		ax-4 2135	. 2 ⊢ (∀xφ → φ)
2		sps-o.1	. 2 ⊢ (φ → ψ)
3	1, 2	syl 15	1 ⊢ (∀xφ → ψ)

Syntax hints:   → wi 4  ∀wal 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-4 2135

This theorem is referenced by:  ax467to6  2171  ax10-16  2190  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  ax10o-o  2203