Metamath Proof Explorer

Theorem prneimg2

Description: Two pairs are not equal if their counterparts are not equal. (Contributed by AV, 5-Sep-2025)

Ref Expression
Assertion prneimg2 ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ D ∈ Y → A B ≠ C D ↔ A ≠ C ∨ B ≠ D ∧ A ≠ D ∨ B ≠ C

Proof

Step Hyp Ref Expression
1 preq12bg ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ D ∈ Y → A B = C D ↔ A = C ∧ B = D ∨ A = D ∧ B = C
2 1 necon3abid ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ D ∈ Y → A B ≠ C D ↔ ¬ A = C ∧ B = D ∨ A = D ∧ B = C
3 ioran ⊢ ¬ A = C ∧ B = D ∨ A = D ∧ B = C ↔ ¬ A = C ∧ B = D ∧ ¬ A = D ∧ B = C
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 ianor ⊢ ¬ A = D ∧ B = C ↔ ¬ A = D ∨ ¬ B = C
10 df-ne ⊢ A ≠ D ↔ ¬ A = D
11 df-ne ⊢ B ≠ C ↔ ¬ B = C
12 10 11 orbi12i ⊢ A ≠ D ∨ B ≠ C ↔ ¬ A = D ∨ ¬ B = C
13 9 12 bitr4i ⊢ ¬ A = D ∧ B = C ↔ A ≠ D ∨ B ≠ C
14 8 13 anbi12i ⊢ ¬ A = C ∧ B = D ∧ ¬ A = D ∧ B = C ↔ A ≠ C ∨ B ≠ D ∧ A ≠ D ∨ B ≠ C
15 3 14 bitri ⊢ ¬ A = C ∧ B = D ∨ A = D ∧ B = C ↔ A ≠ C ∨ B ≠ D ∧ A ≠ D ∨ B ≠ C
16 2 15 bitrdi ⊢ A ∈ U ∧ B ∈ V ∧ C ∈ X ∧ D ∈ Y → A B ≠ C D ↔ A ≠ C ∨ B ≠ D ∧ A ≠ D ∨ B ≠ C