![]() |
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 2993 | 1 ⊢ (𝐴 = 𝐵 → (𝐶 ≠ 𝐴 ↔ 𝐶 ≠ 𝐵)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1533 ≠ wne 2932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-ex 1774 df-cleq 2716 df-ne 2933 |
This theorem is referenced by: psseq2 4081 prproe 4898 fprg 7146 f1dom3el3dif 7261 f1prex 7275 xpord2lem 8123 xpord3lem 8130 dfac5 10120 kmlem4 10145 kmlem14 10155 1re 11212 hashge2el2difr 14440 hashdmpropge2 14442 dvdsle 16252 sgrp2rid2ex 18844 isirred 20313 isnzr2 20412 dmatelnd 22322 mdetdiaglem 22424 mdetunilem1 22438 mdetunilem2 22439 maducoeval2 22466 hausnei 23156 regr1lem2 23568 xrhmeo 24795 axtg5seg 28188 axtgupdim2 28194 axtgeucl 28195 ishlg 28325 tglnpt2 28364 axlowdim1 28689 umgrvad2edg 28942 2pthdlem1 29656 3pthdlem1 29889 upgr3v3e3cycl 29905 upgr4cycl4dv4e 29910 eupth2lem3lem4 29956 3cyclfrgrrn1 30010 4cycl2vnunb 30015 numclwwlkovh 30098 numclwwlkovq 30099 numclwwlk2lem1 30101 numclwlk2lem2f 30102 superpos 32079 signswch 34064 axtgupdim2ALTV 34171 dfrdg4 35419 fvray 35609 linedegen 35611 fvline 35612 linethru 35621 hilbert1.1 35622 knoppndvlem21 35899 poimirlem1 36983 hlsuprexch 38746 3dim1lem5 38831 llni2 38877 lplni2 38902 2llnjN 38932 lvoli2 38946 2lplnj 38985 islinei 39105 cdleme40n 39833 cdlemg33b 40072 ax6e2ndeq 43834 ax6e2ndeqVD 44184 ax6e2ndeqALT 44206 refsum2cnlem1 44235 stoweidlem43 45269 nnfoctbdjlem 45681 elprneb 46249 ichnreuop 46650 inlinecirc02plem 47685 |
Copyright terms: Public domain | W3C validator |