![]() |
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 2941 | . . 3 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | df-ne 2941 | . . 3 ⊢ (𝐶 ≠ 𝐷 ↔ ¬ 𝐶 = 𝐷) | |
3 | 1, 2 | anbi12i 628 | . 2 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ (¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷)) |
4 | pm4.56 988 | . 2 ⊢ ((¬ 𝐴 = 𝐵 ∧ ¬ 𝐶 = 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) | |
5 | 3, 4 | bitri 275 | 1 ⊢ ((𝐴 ≠ 𝐵 ∧ 𝐶 ≠ 𝐷) ↔ ¬ (𝐴 = 𝐵 ∨ 𝐶 = 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 205 ∧ wa 397 ∨ wo 846 = wceq 1542 ≠ wne 2940 |
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 206 df-an 398 df-or 847 df-ne 2941 |
This theorem is referenced by: nelpri 4616 nelprd 4618 eldifpr 4619 0nelop 5454 om00 8523 om00el 8524 oeoe 8547 mulne0b 11801 xmulpnf1 13199 lcmgcd 16488 lcmdvds 16489 drngmulne0 20223 lvecvsn0 20586 domnmuln0 20784 abvn0b 20788 mdetralt 21973 ply1domn 25504 vieta1lem1 25686 vieta1lem2 25687 atandm 26242 atandm3 26244 dchrelbas3 26602 eupth2lem3lem7 29220 frgrreg 29380 nmlno0lem 29777 nmlnop0iALT 30979 chirredi 31378 nelpr 31501 subfacp1lem1 33830 filnetlem4 34899 disjecxrn 36897 lcvbr3 37531 cvrnbtwn4 37787 elpadd0 38318 cdleme0moN 38734 cdleme0nex 38799 fsuppind 40808 isdomn3 41574 lidldomnnring 46314 |
Copyright terms: Public domain | W3C validator |