Metamath Proof Explorer


Theorem neanior

Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007)

Ref Expression
Assertion neanior A B C D ¬ A = B C = D

Proof

Step Hyp Ref Expression
1 df-ne A B ¬ A = B
2 df-ne C D ¬ C = D
3 1 2 anbi12i A B C D ¬ A = B ¬ C = D
4 pm4.56 ¬ A = B ¬ C = D ¬ A = B C = D
5 3 4 bitri A B C D ¬ A = B C = D