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 3017 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | df-ne 3017 | . . 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 3016 |
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 3017 |
This theorem is referenced by: nelpri 4586 nelprd 4588 eldifpr 4589 0nelop 5378 om00 8191 om00el 8192 oeoe 8215 mulne0b 11270 xmulpnf1 12657 lcmgcd 15941 lcmdvds 15942 drngmulne0 19455 lvecvsn0 19812 domnmuln0 20001 abvn0b 20005 mdetralt 21147 ply1domn 24646 vieta1lem1 24828 vieta1lem2 24829 atandm 25381 atandm3 25383 dchrelbas3 25742 eupth2lem3lem7 27941 frgrreg 28101 nmlno0lem 28498 nmlnop0iALT 29700 chirredi 30099 nelpr 30219 subfacp1lem1 32324 filnetlem4 33627 lcvbr3 36041 cvrnbtwn4 36297 elpadd0 36827 cdleme0moN 37243 cdleme0nex 37308 isdomn3 39684 lidldomnnring 44099 |
Copyright terms: Public domain | W3C validator |