Theorem pm13.193

Description: Theorem *13.193 in WhiteheadRussell p. 179. (Contributed by Andrew Salmon, 3-Jun-2011)

	Ref	Expression
Assertion	pm13.193	|- ( ( ph /\ x = y ) <-> ( [ y / x ] ph /\ x = y ) )

Proof

Step	Hyp	Ref	Expression
1		sbequ12	|- ( x = y -> ( ph <-> [ y / x ] ph ) )
2	1	pm5.32ri	|- ( ( ph /\ x = y ) <-> ( [ y / x ] ph /\ x = y ) )