This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbtALT

Description: Alternate proof of sbt , shorter but using additional axioms. (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	⊢ [ 𝑦 / 𝑥 ] 𝜑