Metamath Proof Explorer


Theorem opthneg

Description: Two ordered pairs are not equal iff their first components or their second components are not equal. (Contributed by AV, 13-Dec-2018)

Ref Expression
Assertion opthneg A V B W A B C D A C B D

Proof

Step Hyp Ref Expression
1 df-ne A B C D ¬ A B = C D
2 opthg A V B W A B = C D A = C B = D
3 2 notbid A V B W ¬ A B = C D ¬ A = C B = D
4 ianor ¬ A = C B = D ¬ A = C ¬ B = D
5 df-ne A C ¬ A = C
6 df-ne B D ¬ B = D
7 5 6 orbi12i A C B D ¬ A = C ¬ B = D
8 4 7 bitr4i ¬ A = C B = D A C B D
9 3 8 bitrdi A V B W ¬ A B = C D A C B D
10 1 9 syl5bb A V B W A B C D A C B D