![]() |
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 612 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷)) |
4 | pm4.56 973 | . 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | |
5 | 3, 4 | bitri 264 | 1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 196 ∧ wa 382 ∨ wo 836 = wceq 1631 ≠ 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 197 df-an 383 df-or 837 df-ne 2944 |
This theorem is referenced by: nelpri 4341 nelprd 4343 eldifpr 4344 0nelop 5088 om00 7813 om00el 7814 oeoe 7837 mulne0b 10874 xmulpnf1 12309 lcmgcd 15528 lcmdvds 15529 drngmulne0 18979 lvecvsn0 19322 domnmuln0 19513 abvn0b 19517 mdetralt 20632 ply1domn 24103 vieta1lem1 24285 vieta1lem2 24286 atandm 24824 atandm3 24826 dchrelbas3 25184 eupth2lem3lem7 27414 frgrreg 27593 nmlno0lem 27988 nmlnop0iALT 29194 chirredi 29593 subfacp1lem1 31499 filnetlem4 32713 lcvbr3 34830 cvrnbtwn4 35086 elpadd0 35616 cdleme0moN 36033 cdleme0nex 36098 isdomn3 38306 lidldomnnring 42453 |
Copyright terms: Public domain | W3C validator |