Theorem sbco4lemOLD

Description: Obsolete version of sbco4lem as of 12-Oct-2024. (Contributed by Jim Kingdon, 26-Sep-2018) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

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