Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neorian | Structured version Visualization version GIF version |
Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
Ref | Expression |
---|---|
neorian | ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 3017 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | df-ne 3017 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | orbi12i 908 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷)) |
4 | ianor 975 | . 2 ⊢ (¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷)) | |
5 | 3, 4 | bitr4i 279 | 1 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 ∧ wa 396 ∨ wo 841 = wceq 1528 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-ne 3017 |
This theorem is referenced by: neneor 3118 oeoa 8213 recextlem2 11260 crne0 11620 crreczi 13579 gcdcllem3 15840 bezoutlem2 15878 dsmmacl 20815 txhaus 22185 itg1addlem2 24227 coeaddlem 24768 dcubic 25351 creq0 30398 sibfof 31498 nrhmzr 44042 rrx2pnecoorneor 44600 |
Copyright terms: Public domain | W3C validator |