Metamath Proof Explorer

Theorem neneor

Description: If two classes are different, a third class must be different of at least one of them. (Contributed by Thierry Arnoux, 8-Aug-2020)

Ref Expression
Assertion neneor 
|- ( A =/= B -> ( A =/= C \/ B =/= C ) )

Proof

Step Hyp Ref Expression
1 eqtr3 
 |-  ( ( A = C /\ B = C ) -> A = B )
2 1 necon3ai 
 |-  ( A =/= B -> -. ( A = C /\ B = C ) )
3 neorian 
 |-  ( ( A =/= C \/ B =/= C ) <-> -. ( A = C /\ B = C ) )
4 2 3 sylibr 
 |-  ( A =/= B -> ( A =/= C \/ B =/= C ) )