Metamath Proof Explorer


Theorem sb3bOLD

Description: Obsolete version of sb3b as of 21-Feb-2024. (Contributed by BJ, 6-Oct-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sb3bOLD ¬xx=yyxφxx=yφ

Proof

Step Hyp Ref Expression
1 sb1 yxφxx=yφ
2 sb3 ¬xx=yxx=yφyxφ
3 1 2 impbid2 ¬xx=yyxφxx=yφ