![]() |
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 8143 addneintr2d 8144 negne0bd 8259 negned 8263 subne0d 8275 subne0ad 8277 subneintrd 8310 subneintr2d 8312 qapne 9637 xrlttri3 9795 xaddass2 9868 sqne0 10582 fihashneq0 10769 hashnncl 10770 cjne0 10912 absne0d 11191 sqrt2irraplemnn 12173 ringinvnz1ne0 13179 metn0 13771 lgsabs1 14333 neap0mkv 14698 |
Copyright terms: Public domain | W3C validator |