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

Assertion  neneor   ( A =/= B > ( A =/= C \/ B =/= C ) ) 
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 ) ) 