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 2936 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | df-ne 2936 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | anbi12i 630 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷)) |
4 | pm4.56 988 | . 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | |
5 | 3, 4 | bitri 278 | 1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 209 ∧ wa 399 ∨ wo 846 = wceq 1542 ≠ wne 2935 |
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 210 df-an 400 df-or 847 df-ne 2936 |
This theorem is referenced by: nelpri 4555 nelprd 4557 eldifpr 4558 0nelop 5363 om00 8244 om00el 8245 oeoe 8268 mulne0b 11371 xmulpnf1 12762 lcmgcd 16060 lcmdvds 16061 drngmulne0 19655 lvecvsn0 20012 domnmuln0 20202 abvn0b 20206 mdetralt 21371 ply1domn 24888 vieta1lem1 25070 vieta1lem2 25071 atandm 25626 atandm3 25628 dchrelbas3 25986 eupth2lem3lem7 28183 frgrreg 28343 nmlno0lem 28740 nmlnop0iALT 29942 chirredi 30341 nelpr 30465 subfacp1lem1 32724 filnetlem4 34225 lcvbr3 36692 cvrnbtwn4 36948 elpadd0 37478 cdleme0moN 37894 cdleme0nex 37959 fsuppind 39898 isdomn3 40641 lidldomnnring 45069 |
Copyright terms: Public domain | W3C validator |