![]() |
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 2972 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | df-ne 2972 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | anbi12i 621 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷)) |
4 | pm4.56 1012 | . 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | |
5 | 3, 4 | bitri 267 | 1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 ∧ wa 385 ∨ wo 874 = wceq 1653 ≠ wne 2971 |
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 199 df-an 386 df-or 875 df-ne 2972 |
This theorem is referenced by: nelpri 4393 nelprd 4395 eldifpr 4396 0nelop 5150 om00 7895 om00el 7896 oeoe 7919 mulne0b 10960 xmulpnf1 12353 lcmgcd 15655 lcmdvds 15656 drngmulne0 19087 lvecvsn0 19430 domnmuln0 19621 abvn0b 19625 mdetralt 20740 ply1domn 24224 vieta1lem1 24406 vieta1lem2 24407 atandm 24955 atandm3 24957 dchrelbas3 25315 eupth2lem3lem7 27579 frgrreg 27779 nmlno0lem 28173 nmlnop0iALT 29379 chirredi 29778 subfacp1lem1 31678 filnetlem4 32888 lcvbr3 35044 cvrnbtwn4 35300 elpadd0 35830 cdleme0moN 36246 cdleme0nex 36311 isdomn3 38567 lidldomnnring 42729 |
Copyright terms: Public domain | W3C validator |