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 3076 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 = wceq 1528 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: psseq2 4064 prproe 4830 fprg 6910 f1dom3el3dif 7018 f1prex 7031 dfac5 9543 kmlem4 9568 kmlem14 9578 1re 10630 hashge2el2difr 13829 hashdmpropge2 13831 dvdsle 15650 sgrp2rid2ex 18032 isirred 19380 isnzr2 19966 dmatelnd 21035 mdetdiaglem 21137 mdetunilem1 21151 mdetunilem2 21152 maducoeval2 21179 hausnei 21866 regr1lem2 22278 xrhmeo 23479 axtg5seg 26179 axtgupdim2 26185 axtgeucl 26186 ishlg 26316 tglnpt2 26355 axlowdim1 26673 umgrvad2edg 26923 2pthdlem1 27637 3pthdlem1 27871 upgr3v3e3cycl 27887 upgr4cycl4dv4e 27892 eupth2lem3lem4 27938 3cyclfrgrrn1 27992 4cycl2vnunb 27997 numclwwlkovh 28080 numclwwlkovq 28081 numclwwlk2lem1 28083 numclwlk2lem2f 28084 superpos 30059 signswch 31731 axtgupdim2ALTV 31839 dfrdg4 33310 fvray 33500 linedegen 33502 fvline 33503 linethru 33512 hilbert1.1 33513 knoppndvlem21 33769 poimirlem1 34775 hlsuprexch 36399 3dim1lem5 36484 llni2 36530 lplni2 36555 2llnjN 36585 lvoli2 36599 2lplnj 36638 islinei 36758 cdleme40n 37486 cdlemg33b 37725 ax6e2ndeq 40773 ax6e2ndeqVD 41123 ax6e2ndeqALT 41145 refsum2cnlem1 41174 stoweidlem43 42209 nnfoctbdjlem 42618 elprneb 43145 ichnreuop 43481 inlinecirc02plem 44671 |
Copyright terms: Public domain | W3C validator |