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	$⊢ [y/ x] φ$

Proof

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