Metamath Proof Explorer

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 ⊢ y u x v u x v y φ ↔ x w y x w y φ

Proof

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