Theorem sbtALT

Description: Alternate proof of sbt , shorter but using ax-4 and ax-5 . (Contributed by NM, 21-Jan-2004) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sbtALT.1	|- ph
Assertion	sbtALT	|- [ y / x ] ph

Proof

Step	Hyp	Ref	Expression
1		sbtALT.1	|- ph
2		stdpc4	|- ( A. x ph -> [ y / x ] ph )
3	2 1	mpg	|- [ y / x ] ph