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 2627 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | 2 | necon3bii 2846 | 1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 = wceq 1483 ≠ wne 2794 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-an 386 df-ex 1705 df-cleq 2615 df-ne 2795 |
This theorem is referenced by: eqnetri 2864 rabn0OLD 3959 exss 4931 inisegn0 5497 suppvalbr 7299 brwitnlem 7587 en3lplem2 8512 hta 8760 kmlem3 8974 domtriomlem 9264 zorn2lem6 9323 konigthlem 9390 rpnnen1lem2 11814 rpnnen1lem1 11815 rpnnen1lem3 11816 rpnnen1lem5 11818 rpnnen1lem1OLD 11821 rpnnen1lem3OLD 11822 rpnnen1lem5OLD 11824 fsuppmapnn0fiubex 12792 seqf1olem1 12840 iscyg2 18284 gsumval3lem2 18307 opprirred 18702 ptclsg 21418 iscusp2 22106 dchrptlem1 24989 dchrptlem2 24990 disjex 29405 disjexc 29406 signsply0 30628 signstfveq0a 30653 bnj1177 31074 bnj1253 31085 fin2so 33396 stoweidlem36 40253 aovnuoveq 41271 aovovn0oveq 41274 ovn0dmfun 41764 aacllem 42547 |
Copyright terms: Public domain | W3C validator |