![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > necon3bid | GIF version |
Description: Deduction from equality to inequality. (Contributed by NM, 23-Feb-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) |
Ref | Expression |
---|---|
necon3bid.1 | ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) |
Ref | Expression |
---|---|
necon3bid | ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2348 | . 2 ⊢ (𝐴 ≠ 𝐵 ↔ ¬ 𝐴 = 𝐵) | |
2 | necon3bid.1 | . . 3 ⊢ (𝜑 → (𝐴 = 𝐵 ↔ 𝐶 = 𝐷)) | |
3 | 2 | necon3bbid 2387 | . 2 ⊢ (𝜑 → (¬ 𝐴 = 𝐵 ↔ 𝐶 ≠ 𝐷)) |
4 | 1, 3 | bitrid 192 | 1 ⊢ (𝜑 → (𝐴 ≠ 𝐵 ↔ 𝐶 ≠ 𝐷)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 105 = wceq 1353 ≠ wne 2347 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 |
This theorem depends on definitions: df-bi 117 df-ne 2348 |
This theorem is referenced by: nebidc 2427 addneintrd 8147 addneintr2d 8148 negne0bd 8263 negned 8267 subne0d 8279 subne0ad 8281 subneintrd 8314 subneintr2d 8316 qapne 9641 xrlttri3 9799 xaddass2 9872 sqne0 10588 fihashneq0 10776 hashnncl 10777 cjne0 10919 absne0d 11198 sqrt2irraplemnn 12181 ringinvnz1ne0 13231 metn0 13917 lgsabs1 14479 neap0mkv 14856 |
Copyright terms: Public domain | W3C validator |