Metamath Proof Explorer

Theorem bj-sbidmOLD

Description: Obsolete proof of sbidm temporarily kept here to check it gives no additional insight. (Contributed by NM, 8-Mar-1995) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-sbidmOLD ⊢ y x y x φ ↔ y x φ

Proof

Step Hyp Ref Expression
1 equsb2 ⊢ y x y = x
2 sbequ12r ⊢ y = x → y x φ ↔ φ
3 2 sbimi ⊢ y x y = x → y x y x φ ↔ φ
4 1 3 ax-mp ⊢ y x y x φ ↔ φ
5 sbbi ⊢ y x y x φ ↔ φ ↔ y x y x φ ↔ y x φ
6 4 5 mpbi ⊢ y x y x φ ↔ y x φ