Theorem sbco4lem

Description: Lemma for sbco4 . It replaces the temporary variable v with another temporary variable w . (Contributed by Jim Kingdon, 26-Sep-2018) (Proof shortened by Wolf Lammen, 12-Oct-2024)

	Ref	Expression
Assertion	sbco4lem	|- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )

Proof

Step	Hyp	Ref	Expression
1		sbcom2	|- ( [ y / x ] [ v / w ] [ w / y ] ph <-> [ v / w ] [ y / x ] [ w / y ] ph )
2	1	sbbii	|- ( [ x / v ] [ y / x ] [ v / w ] [ w / y ] ph <-> [ x / v ] [ v / w ] [ y / x ] [ w / y ] ph )
3		sbco2vv	|- ( [ v / w ] [ w / y ] ph <-> [ v / y ] ph )
4	3	2sbbii	|- ( [ x / v ] [ y / x ] [ v / w ] [ w / y ] ph <-> [ x / v ] [ y / x ] [ v / y ] ph )
5		sbco2vv	|- ( [ x / v ] [ v / w ] [ y / x ] [ w / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )
6	2 4 5	3bitr3i	|- ( [ x / v ] [ y / x ] [ v / y ] ph <-> [ x / w ] [ y / x ] [ w / y ] ph )