![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > neeq1 | GIF version |
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) |
Ref | Expression |
---|---|
neeq1 | ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2194 | . . 3 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶)) | |
2 | 1 | notbid 668 | . 2 ⊢ (𝐴 = 𝐵 → (¬ 𝐴 = 𝐶 ↔ ¬ 𝐵 = 𝐶)) |
3 | df-ne 2358 | . 2 ⊢ (𝐴 ≠ 𝐶 ↔ ¬ 𝐴 = 𝐶) | |
4 | df-ne 2358 | . 2 ⊢ (𝐵 ≠ 𝐶 ↔ ¬ 𝐵 = 𝐶) | |
5 | 2, 3, 4 | 3bitr4g 223 | 1 ⊢ (𝐴 = 𝐵 → (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 105 = wceq 1363 ≠ wne 2357 |
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 615 ax-in2 616 ax-5 1457 ax-gen 1459 ax-4 1520 ax-17 1536 ax-ext 2169 |
This theorem depends on definitions: df-bi 117 df-cleq 2180 df-ne 2358 |
This theorem is referenced by: neeq1i 2372 neeq1d 2375 nelrdva 2956 disji2 4008 0inp0 4178 frecabcl 6414 fiintim 6942 eldju2ndl 7085 updjudhf 7092 netap 7267 2oneel 7269 2omotaplemap 7270 2omotaplemst 7271 exmidapne 7273 xnn0nemnf 9264 uzn0 9557 xrnemnf 9791 xrnepnf 9792 ngtmnft 9831 xsubge0 9895 xposdif 9896 xleaddadd 9901 fztpval 10097 pcpre1 12306 pcqmul 12317 pcqcl 12320 xpsfrnel 12782 fiinopn 13857 neapmkv 15170 neap0mkv 15171 ltlenmkv 15172 |
Copyright terms: Public domain | W3C validator |