New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > neeq1 | GIF version |
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) |
Ref | Expression |
---|---|
neeq1 | ⊢ (A = B → (A ≠ C ↔ B ≠ C)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq1 2359 | . . 3 ⊢ (A = B → (A = C ↔ B = C)) | |
2 | 1 | notbid 285 | . 2 ⊢ (A = B → (¬ A = C ↔ ¬ B = C)) |
3 | df-ne 2518 | . 2 ⊢ (A ≠ C ↔ ¬ A = C) | |
4 | df-ne 2518 | . 2 ⊢ (B ≠ C ↔ ¬ B = C) | |
5 | 2, 3, 4 | 3bitr4g 279 | 1 ⊢ (A = B → (A ≠ C ↔ B ≠ C)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 176 = wceq 1642 ≠ wne 2516 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-11 1746 ax-ext 2334 |
This theorem depends on definitions: df-bi 177 df-ex 1542 df-cleq 2346 df-ne 2518 |
This theorem is referenced by: neeq1i 2526 neeq1d 2529 psseq1 3356 opkltfing 4449 ltfintri 4466 tfin11 4493 0ceven 4505 evennn 4506 oddnn 4507 evennnul 4508 oddnnul 4509 sucevenodd 4510 sucoddeven 4511 dfevenfin2 4512 dfoddfin2 4513 evenoddnnnul 4514 evenodddisjlem1 4515 eventfin 4517 oddtfin 4518 nulnnn 4556 xp11 5056 tz6.12i 5348 frd 5922 elqsn0 5993 enprmapc 6083 ce2 6192 nchoicelem14 6302 |
Copyright terms: Public domain | W3C validator |