Metamath Proof Explorer

Theorem sbco4lem

Description: Lemma for sbco4 . It replaces the temporary variable v with another temporary variable w . (Contributed by Jim Kingdon, 26-Sep-2018)

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

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