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 2615 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | 2 | necon3bii 2834 | 1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 = wceq 1475 ≠ wne 2780 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-cleq 2603 df-ne 2782 |
This theorem is referenced by: eqnetri 2852 rabn0OLD 3913 exss 4858 inisegn0 5416 suppvalbr 7186 brwitnlem 7474 en3lplem2 8395 hta 8643 kmlem3 8857 domtriomlem 9147 zorn2lem6 9206 konigthlem 9269 rpnnen1lem2 11690 rpnnen1lem1 11691 rpnnen1lem3 11692 rpnnen1lem5 11694 rpnnen1lem1OLD 11697 rpnnen1lem3OLD 11698 rpnnen1lem5OLD 11700 fsuppmapnn0fiubex 12654 seqf1olem1 12702 iscyg2 18107 gsumval3lem2 18130 opprirred 18525 ptclsg 21228 iscusp2 21916 dchrptlem1 24789 dchrptlem2 24790 disjex 28787 disjexc 28788 signsply0 29954 signstfveq0a 29979 bnj1177 30328 bnj1253 30339 fin2so 32566 stoweidlem36 38929 aovnuoveq 39920 aovovn0oveq 39923 ovn0dmfun 41554 aacllem 42356 |
Copyright terms: Public domain | W3C validator |