![]() |
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 2939 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | df-ne 2939 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | orbi12i 914 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷)) |
4 | ianor 983 | . 2 ⊢ (¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷)) | |
5 | 3, 4 | bitr4i 278 | 1 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1537 ≠ wne 2938 |
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 207 df-an 396 df-or 848 df-ne 2939 |
This theorem is referenced by: neneor 3040 poxp2 8167 oeoa 8634 recextlem2 11892 crne0 12257 crreczi 14264 gcdcllem3 16535 bezoutlem2 16574 nrhmzr 20554 dsmmacl 21779 mhpmulcl 22171 txhaus 23671 itg1addlem2 25746 coeaddlem 26303 dcubic 26904 creq0 32753 sibfof 34322 rrx2pnecoorneor 48565 |
Copyright terms: Public domain | W3C validator |