Theorem sbco4

Description: Two ways of exchanging two variables. Both sides of the biconditional exchange x and y , either via two temporary variables u and v , or a single temporary w . (Contributed by Jim Kingdon, 25-Sep-2018)

	Ref	Expression
Assertion	sbco4	$$⊢\left[y/u\right]\left[x/v\right]\left[u/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[x/v\right]\left[y/u\right]\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \left[y/u\right]\left[x/v\right]\left[u/x\right]\left[v/y\right]\phi$$
2		sbco2vv	$$⊢\left[y/u\right]\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \left[y/x\right]\left[v/y\right]\phi$$
3	2	sbbii	$$⊢\left[x/v\right]\left[y/u\right]\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \left[x/v\right]\left[y/x\right]\left[v/y\right]\phi$$
4	1 3	bitr3i	$$⊢\left[y/u\right]\left[x/v\right]\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \left[x/v\right]\left[y/x\right]\left[v/y\right]\phi$$
5		sbco4lem	$$⊢\left[x/v\right]\left[y/x\right]\left[v/y\right]\phi \leftrightarrow \left[x/t\right]\left[y/x\right]\left[t/y\right]\phi$$
6		sbco4lem	$$⊢\left[x/t\right]\left[y/x\right]\left[t/y\right]\phi \leftrightarrow \left[x/w\right]\left[y/x\right]\left[w/y\right]\phi$$
7	4 5 6	3bitri	$$⊢\left[y/u\right]\left[x/v\right]\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \left[x/w\right]\left[y/x\right]\left[w/y\right]\phi$$