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) (Proof shortened by Wolf Lammen, 12-Oct-2024)

Ref Expression
Assertion sbco4lem ⊢ x v y x v y φ ↔ x w y x w y φ

Proof

Step Hyp Ref Expression
1 sbcom2 ⊢ y x v w w y φ ↔ v w y x w y φ
2 1 sbbii ⊢ x v y x v w w y φ ↔ x v v w y x w y φ
3 sbco2vv ⊢ v w w y φ ↔ v y φ
4 3 2sbbii ⊢ x v y x v w w y φ ↔ x v y x v y φ
5 sbco2vv ⊢ x v v w y x w y φ ↔ x w y x w y φ
6 2 4 5 3bitr3i ⊢ x v y x v y φ ↔ x w y x w y φ