This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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