|   | 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 915 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷)) | 
| 4 | ianor 984 | . 2 ⊢ (¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷) ↔ (¬ 𝐴 = 𝐵 ∨ ¬ 𝐶 = 𝐷)) | |
| 5 | 3, 4 | bitr4i 278 | 1 ⊢ ((𝐴 ≠ 𝐵 ∨ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∧ 𝐶 = 𝐷)) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ¬ wn 3 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1540 ≠ 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 207 df-an 396 df-or 849 df-ne 2941 | 
| This theorem is referenced by: neneor 3042 poxp2 8168 oeoa 8635 recextlem2 11894 crne0 12259 crreczi 14267 gcdcllem3 16538 bezoutlem2 16577 nrhmzr 20537 dsmmacl 21761 mhpmulcl 22153 txhaus 23655 itg1addlem2 25732 coeaddlem 26288 dcubic 26889 creq0 32746 sibfof 34342 rrx2pnecoorneor 48636 | 
| Copyright terms: Public domain | W3C validator |