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	$$⊢\left[x/v\right]\left[y/x\right]\left[v/y\right]\phi \leftrightarrow \left[x/w\right]\left[y/x\right]\left[w/y\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbcom2	$$⊢\left[y/x\right]\left[v/w\right]\left[w/y\right]\phi \leftrightarrow \left[v/w\right]\left[y/x\right]\left[w/y\right]\phi$$
2	1	sbbii	$$⊢\left[x/v\right]\left[y/x\right]\left[v/w\right]\left[w/y\right]\phi \leftrightarrow \left[x/v\right]\left[v/w\right]\left[y/x\right]\left[w/y\right]\phi$$
3		sbco2vv	$$⊢\left[v/w\right]\left[w/y\right]\phi \leftrightarrow \left[v/y\right]\phi$$
4	3	2sbbii	$$⊢\left[x/v\right]\left[y/x\right]\left[v/w\right]\left[w/y\right]\phi \leftrightarrow \left[x/v\right]\left[y/x\right]\left[v/y\right]\phi$$
5		sbco2vv	$$⊢\left[x/v\right]\left[v/w\right]\left[y/x\right]\left[w/y\right]\phi \leftrightarrow \left[x/w\right]\left[y/x\right]\left[w/y\right]\phi$$
6	2 4 5	3bitr3i	$$⊢\left[x/v\right]\left[y/x\right]\left[v/y\right]\phi \leftrightarrow \left[x/w\right]\left[y/x\right]\left[w/y\right]\phi$$