![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > neeq1i | Structured version Visualization version GIF version |
Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.) |
Ref | Expression |
---|---|
neeq1i.1 | ⊢ 𝐴 = 𝐵 |
Ref | Expression |
---|---|
neeq1i | ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | neeq1i.1 | . . 3 ⊢ 𝐴 = 𝐵 | |
2 | 1 | eqeq1i 2731 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | 2 | necon3bii 2983 | 1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1534 ≠ wne 2930 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-ne 2931 |
This theorem is referenced by: eqnetri 3001 exss 5471 inisegn0 6110 suppvalbr 8180 brwitnlem 8539 en3lplem2 9658 hta 9942 kmlem3 10197 domtriomlem 10487 zorn2lem6 10546 konigthlem 10613 rpnnen1lem2 13015 rpnnen1lem1 13016 rpnnen1lem3 13017 rpnnen1lem5 13019 fsuppmapnn0fiubex 14014 seqf1olem1 14063 iscyg2 19882 gsumval3lem2 19906 opprirred 20406 ptclsg 23613 iscusp2 24301 dchrptlem1 27296 dchrptlem2 27297 disjex 32514 disjexc 32515 ufdprmidl 33418 signsply0 34399 signstfveq0a 34424 bnj1177 34853 bnj1253 34864 fin2so 37310 br2coss 38138 stoweidlem36 45675 aovnuoveq 46822 aovovn0oveq 46825 ovn0dmfun 47551 rrx2pnedifcoorneor 48122 2itscp 48187 aacllem 48567 |
Copyright terms: Public domain | W3C validator |