This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sbco4lemOLD

Description: Obsolete version of sbco4lem as of 3-Sep-2025. (Contributed by Jim Kingdon, 26-Sep-2018) (Proof shortened by Wolf Lammen, 12-Oct-2024) (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 2sbbii ⊢ ( [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑤 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 )
5 sbco2vv ⊢ ( [ 𝑥 / 𝑣 ] [ 𝑣 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )
6 2 4 5 3bitr3i ⊢ ( [ 𝑥 / 𝑣 ] [ 𝑦 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑤 ] [ 𝑦 / 𝑥 ] [ 𝑤 / 𝑦 ] 𝜑 )