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

Metamath Proof Explorer

Theorem pm13.13b

Description: Theorem *13.13 in WhiteheadRussell p. 178 with different variable substitution. (Contributed by Andrew Salmon, 3-Jun-2011)

		Ref	Expression
	Assertion	pm13.13b	$⊢ (\underset{˙}{[} A / x \underset{˙}{]} φ \land x = A) \to φ$

Step	Hyp	Ref	Expression
1		sbceq1a	$⊢ x = A \to (φ \leftrightarrow \underset{˙}{[} A / x \underset{˙}{]} φ)$
2	1	biimparc	$⊢ (\underset{˙}{[} A / x \underset{˙}{]} φ \land x = A) \to φ$