Theorem sbco4OLD

Description: Obsolete version of sbco4 as of 3-Sep-2025. (Contributed by Jim Kingdon, 25-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	sbco4OLD	⊢ ( [ 𝑦 / 𝑢 ] [ 𝑥 / 𝑣 ] [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )

Proof

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