Description: Theorem *13.18 in WhiteheadRussell p. 178. (Contributed by Andrew Salmon, 3Jun2011) (Proof shortened by Wolf Lammen, 14May2023)
Ref  Expression  

Assertion  pm13.18   ( ( A = B /\ A =/= C ) > B =/= C ) 
Step  Hyp  Ref  Expression 

1  neeq1   ( A = B > ( A =/= C <> B =/= C ) ) 

2  1  biimpd   ( A = B > ( A =/= C > B =/= C ) ) 
3  2  imp   ( ( A = B /\ A =/= C ) > B =/= C ) 