![]() |
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 2941 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | df-ne 2941 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | orbi12i 914 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷)) |
4 | ianor 981 | . 2 ⊢ (¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷)) | |
5 | 3, 4 | bitr4i 278 | 1 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 397 ∨ wo 846 = wceq 1542 ≠ wne 2940 |
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 206 df-an 398 df-or 847 df-ne 2941 |
This theorem is referenced by: neneor 3041 poxp2 8076 oeoa 8545 recextlem2 11791 crne0 12151 crreczi 14137 gcdcllem3 16386 bezoutlem2 16426 dsmmacl 21163 mhpmulcl 21555 txhaus 23014 itg1addlem2 25077 coeaddlem 25626 dcubic 26212 creq0 31699 sibfof 32997 nrhmzr 46257 rrx2pnecoorneor 46887 |
Copyright terms: Public domain | W3C validator |