Metamath Proof Explorer


Theorem sb1OLD

Description: Obsolete version of sb1 as of 21-Feb-2024. (Contributed by NM, 13-May-1993) Revise df-sb . (Revised by Wolf Lammen, 29-Jul-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sb1OLD yxφxx=yφ

Proof

Step Hyp Ref Expression
1 sbequ2 x=yyxφφ
2 19.8a x=yφxx=yφ
3 2 ex x=yφxx=yφ
4 1 3 syld x=yyxφxx=yφ
5 4 sps xx=yyxφxx=yφ
6 sb4b ¬xx=yyxφxx=yφ
7 equs4 xx=yφxx=yφ
8 6 7 syl6bi ¬xx=yyxφxx=yφ
9 5 8 pm2.61i yxφxx=yφ