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	⊢ 𝜑
Assertion	sbtALT	⊢ [ 𝑦 / 𝑥 ] 𝜑

Proof

Step	Hyp	Ref	Expression
1		sbtALT.1	⊢ 𝜑
2		stdpc4	⊢ ( ∀ 𝑥 𝜑 → [ 𝑦 / 𝑥 ] 𝜑 )
3	2 1	mpg	⊢ [ 𝑦 / 𝑥 ] 𝜑