![]() |
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 3029 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1601 ≠ wne 2969 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-cleq 2770 df-ne 2970 |
This theorem is referenced by: psseq2 3917 prproe 4671 fprg 6690 f1dom3el3dif 6800 f1prex 6813 dfac5 9286 kmlem4 9312 kmlem14 9322 1re 10378 hashge2el2difr 13581 hashdmpropge2 13583 dvdsle 15443 sgrp2rid2ex 17805 isirred 19090 isnzr2 19664 dmatelnd 20711 mdetdiaglem 20813 mdetunilem1 20827 mdetunilem2 20828 maducoeval2 20855 hausnei 21544 regr1lem2 21956 xrhmeo 23157 axtg5seg 25820 axtgupdim2 25826 axtgeucl 25827 ishlg 25957 tglnpt2 25996 axlowdim1 26312 umgrvad2edg 26563 2pthdlem1 27314 3pthdlem1 27571 upgr3v3e3cycl 27587 upgr4cycl4dv4e 27592 eupth2lem3lem4 27639 3cyclfrgrrn1 27697 4cycl2vnunb 27702 numclwwlkovh 27805 numclwwlkovq 27806 numclwwlk2lem1 27808 numclwlk2lem2f 27809 numclwlk2lem2fOLD 27812 superpos 29789 signswch 31242 axtgupdim2OLD 31352 dfrdg4 32651 fvray 32841 linedegen 32843 fvline 32844 linethru 32853 hilbert1.1 32854 knoppndvlem21 33109 poimirlem1 34041 hlsuprexch 35540 3dim1lem5 35625 llni2 35671 lplni2 35696 2llnjN 35726 lvoli2 35740 2lplnj 35779 islinei 35899 cdleme40n 36627 cdlemg33b 36866 ax6e2ndeq 39729 ax6e2ndeqVD 40088 ax6e2ndeqALT 40110 refsum2cnlem1 40139 stoweidlem43 41197 nnfoctbdjlem 41606 elprneb 42108 inlinecirc02plem 43532 |
Copyright terms: Public domain | W3C validator |