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	|- (ph -> ps)

Assertion

Ref	Expression
sps-o	|- (A.xph -> ps)

Proof of Theorem sps-o

Step	Hyp	Ref	Expression
1		ax-4 2135	. 2 |- (A.xph -> ph)
2		sps-o.1	. 2 |- (ph -> ps)
3	1, 2	syl 15	1 |- (A.xph -> ps)

Syntax hints:   -> wi 4  A.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