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

Metamath Proof Explorer

Theorem sbequ12

Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993)

		Ref	Expression
	Assertion	sbequ12	$⊢ x = y \to (φ \leftrightarrow [y/ x] φ)$

Step	Hyp	Ref	Expression
1		sbequ1	$⊢ x = y \to (φ \to [y/ x] φ)$
2		sbequ2	$⊢ x = y \to ([y/ x] φ \to φ)$
3	1 2	impbid	$⊢ x = y \to (φ \leftrightarrow [y/ x] φ)$