Metamath Proof Explorer

Theorem pm13.18

Description: Theorem *13.18 in WhiteheadRussell p. 178. (Contributed by Andrew Salmon, 3-Jun-2011) (Proof shortened by Wolf Lammen, 14-May-2023)

Ref Expression
Assertion pm13.18 
|- ( ( A = B /\ A =/= C ) -> B =/= C )

Proof

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 )