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

Metamath Proof Explorer

Theorem bj-ssbid1

Description: A special case of sbequ1 . (Contributed by BJ, 22-Dec-2020)

		Ref	Expression
	Assertion	bj-ssbid1	$⊢ φ \to [x/ x] φ$

Step	Hyp	Ref	Expression
1		equid	$⊢ x = x$
2		sbequ1	$⊢ x = x \to (φ \to [x/ x] φ)$
3	1 2	ax-mp	$⊢ φ \to [x/ x] φ$