![]() |
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 2738 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | 2 | necon3bii 2993 | 1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 = wceq 1542 ≠ wne 2940 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-cleq 2725 df-ne 2941 |
This theorem is referenced by: eqnetri 3011 exss 5421 inisegn0 6051 suppvalbr 8097 brwitnlem 8454 en3lplem2 9554 hta 9838 kmlem3 10093 domtriomlem 10383 zorn2lem6 10442 konigthlem 10509 rpnnen1lem2 12907 rpnnen1lem1 12908 rpnnen1lem3 12909 rpnnen1lem5 12911 fsuppmapnn0fiubex 13903 seqf1olem1 13953 iscyg2 19664 gsumval3lem2 19688 opprirred 20138 ptclsg 22982 iscusp2 23670 dchrptlem1 26628 dchrptlem2 26629 disjex 31556 disjexc 31557 signsply0 33220 signstfveq0a 33245 bnj1177 33675 bnj1253 33686 fin2so 36111 br2coss 36946 stoweidlem36 44363 aovnuoveq 45509 aovovn0oveq 45512 ovn0dmfun 46144 rrx2pnedifcoorneor 46888 2itscp 46953 aacllem 47334 |
Copyright terms: Public domain | W3C validator |