Theorem pm13.194

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

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

Proof

Step	Hyp	Ref	Expression
1		pm13.13a	|- ( ( ph /\ x = y ) -> [. y / x ]. ph )
2		sbsbc	|- ( [ y / x ] ph <-> [. y / x ]. ph )
3	1 2	sylibr	|- ( ( ph /\ x = y ) -> [ y / x ] ph )
4		simpl	|- ( ( ph /\ x = y ) -> ph )
5		simpr	|- ( ( ph /\ x = y ) -> x = y )
6	3 4 5	3jca	|- ( ( ph /\ x = y ) -> ( [ y / x ] ph /\ ph /\ x = y ) )
7		3simpc	|- ( ( [ y / x ] ph /\ ph /\ x = y ) -> ( ph /\ x = y ) )
8	6 7	impbii	|- ( ( ph /\ x = y ) <-> ( [ y / x ] ph /\ ph /\ x = y ) )