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	⊢ ( 𝐴 ≠ 𝐵 → ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		eqtr3	⊢ ( ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) → 𝐴 = 𝐵 )
2	1	necon3ai	⊢ ( 𝐴 ≠ 𝐵 → ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) )
3		neorian	⊢ ( ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐶 ) ↔ ¬ ( 𝐴 = 𝐶 ∧ 𝐵 = 𝐶 ) )
4	2 3	sylibr	⊢ ( 𝐴 ≠ 𝐵 → ( 𝐴 ≠ 𝐶 ∨ 𝐵 ≠ 𝐶 ) )