Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > neeq2 | Structured version Visualization version GIF version |
Description: Equality theorem for inequality. (Contributed by NM, 19-Nov-1994.) (Proof shortened by Wolf Lammen, 18-Nov-2019.) |
Ref | Expression |
---|---|
neeq2 | ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | id 22 | . 2 ⊢ (𝐴 = 𝐵 → 𝐴 = 𝐵) | |
2 | 1 | neeq2d 2854 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1483 ≠ wne 2794 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-ne 2795 |
This theorem is referenced by: psseq2 3695 prproe 4434 fprg 6422 f1dom3el3dif 6526 f1prex 6539 dfac5 8951 kmlem4 8975 kmlem14 8985 1re 10039 hashge2el2difr 13263 hashdmpropge2 13265 dvdsle 15032 sgrp2rid2ex 17414 isirred 18699 isnzr2 19263 dmatelnd 20302 mdetdiaglem 20404 mdetunilem1 20418 mdetunilem2 20419 maducoeval2 20446 hausnei 21132 regr1lem2 21543 xrhmeo 22745 axtg5seg 25364 axtgupdim2 25370 axtgeucl 25371 ishlg 25497 tglnpt2 25536 axlowdim1 25839 structgrssvtxlemOLD 25915 umgrvad2edg 26105 2pthdlem1 26826 clwwlknclwwlkdifs 26873 3pthdlem1 27024 upgr3v3e3cycl 27040 upgr4cycl4dv4e 27045 eupth2lem3lem4 27091 3cyclfrgrrn1 27149 4cycl2vnunb 27154 numclwwlkovq 27232 numclwwlk2lem1 27235 numclwlk2lem2f 27236 superpos 29213 signswch 30638 axtgupdim2OLD 30746 dfrdg4 32058 fvray 32248 linedegen 32250 fvline 32251 linethru 32260 hilbert1.1 32261 knoppndvlem21 32523 poimirlem1 33410 hlsuprexch 34667 3dim1lem5 34752 llni2 34798 lplni2 34823 2llnjN 34853 lvoli2 34867 2lplnj 34906 islinei 35026 cdleme40n 35756 cdlemg33b 35995 ax6e2ndeq 38775 ax6e2ndeqVD 39145 ax6e2ndeqALT 39167 refsum2cnlem1 39196 stoweidlem43 40260 nnfoctbdjlem 40672 elprneb 41296 |
Copyright terms: Public domain | W3C validator |