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	$$⊢\phi$$
Assertion	sbtALT	$$⊢\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbtALT.1	$$⊢\phi$$
2		stdpc4	$$⊢\forall x\phi \to \left[y/x\right]\phi$$
3	2 1	mpg	$$⊢\left[y/x\right]\phi$$