Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neanior | Structured version Visualization version GIF version |
Description: A De Morgan's law for inequality. (Contributed by NM, 18-May-2007.) |
Ref | Expression |
---|---|
neanior | ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2944 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | df-ne 2944 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | anbi12i 627 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷)) |
4 | pm4.56 986 | . 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | |
5 | 3, 4 | bitri 274 | 1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 396 ∨ wo 844 = wceq 1539 ≠ wne 2943 |
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 397 df-or 845 df-ne 2944 |
This theorem is referenced by: nelpri 4590 nelprd 4592 eldifpr 4593 0nelop 5410 om00 8406 om00el 8407 oeoe 8430 mulne0b 11616 xmulpnf1 13008 lcmgcd 16312 lcmdvds 16313 drngmulne0 20013 lvecvsn0 20371 domnmuln0 20569 abvn0b 20573 mdetralt 21757 ply1domn 25288 vieta1lem1 25470 vieta1lem2 25471 atandm 26026 atandm3 26028 dchrelbas3 26386 eupth2lem3lem7 28598 frgrreg 28758 nmlno0lem 29155 nmlnop0iALT 30357 chirredi 30756 nelpr 30879 subfacp1lem1 33141 filnetlem4 34570 lcvbr3 37037 cvrnbtwn4 37293 elpadd0 37823 cdleme0moN 38239 cdleme0nex 38304 fsuppind 40279 isdomn3 41029 lidldomnnring 45488 |
Copyright terms: Public domain | W3C validator |