Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 sbcom2 ⊢ w v y x v w w y φ ↔ y x w v v w w y φ
2 1 sbbii ⊢ x w w v y x v w w y φ ↔ x w y x w v v w w y φ
3 sbco2vv ⊢ v w w y φ ↔ v y φ
4 3 sbbii ⊢ y x v w w y φ ↔ y x v y φ
5 4 2sbbii ⊢ x w w v y x v w w y φ ↔ x w w v y x v y φ
6 sbco2vv ⊢ x w w v y x v y φ ↔ x v y x v y φ
7 5 6 bitri ⊢ x w w v y x v w w y φ ↔ x v y x v y φ
8 sbid2vw ⊢ w v v w w y φ ↔ w y φ
9 8 2sbbii ⊢ x w y x w v v w w y φ ↔ x w y x w y φ
10 2 7 9 3bitr3i ⊢ x v y x v y φ ↔ x w y x w y φ