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	⊢ ( [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sbcom2	⊢ ( [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑣 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
2	1	sbbii	⊢ ( [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑣 ] [ 𝑣 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
3		sbco2vv	⊢ ( [ 𝑣 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑣 / 𝑦 ] 𝜑 )
4	3	2sbbii	⊢ ( [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
5		sbco2vv	⊢ ( [ 𝑥 / 𝑣 ] [ 𝑣 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
6	2 4 5	3bitr3i	⊢ ( [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )