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 3014 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | df-ne 3014 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | anbi12i 626 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷)) |
4 | pm4.56 982 | . 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | |
5 | 3, 4 | bitri 276 | 1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 207 ∧ wa 396 ∨ wo 841 = wceq 1528 ≠ wne 3013 |
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 208 df-an 397 df-or 842 df-ne 3014 |
This theorem is referenced by: nelpri 4584 nelprd 4586 eldifpr 4587 0nelop 5377 om00 8190 om00el 8191 oeoe 8214 mulne0b 11269 xmulpnf1 12655 lcmgcd 15939 lcmdvds 15940 drngmulne0 19453 lvecvsn0 19810 domnmuln0 19999 abvn0b 20003 mdetralt 21145 ply1domn 24644 vieta1lem1 24826 vieta1lem2 24827 atandm 25381 atandm3 25383 dchrelbas3 25741 eupth2lem3lem7 27940 frgrreg 28100 nmlno0lem 28497 nmlnop0iALT 29699 chirredi 30098 nelpr 30218 subfacp1lem1 32323 filnetlem4 33626 lcvbr3 36039 cvrnbtwn4 36295 elpadd0 36825 cdleme0moN 37241 cdleme0nex 37306 isdomn3 39682 lidldomnnring 44129 |
Copyright terms: Public domain | W3C validator |