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 2826 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | 2 | necon3bii 3068 | 1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1528 ≠ wne 3016 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2793 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-cleq 2814 df-ne 3017 |
This theorem is referenced by: eqnetri 3086 exss 5347 inisegn0 5955 suppvalbr 7825 brwitnlem 8123 en3lplem2 9065 hta 9315 kmlem3 9567 domtriomlem 9853 zorn2lem6 9912 konigthlem 9979 rpnnen1lem2 12366 rpnnen1lem1 12367 rpnnen1lem3 12368 rpnnen1lem5 12370 fsuppmapnn0fiubex 13350 seqf1olem1 13399 iscyg2 18932 gsumval3lem2 18957 opprirred 19383 ptclsg 22153 iscusp2 22840 dchrptlem1 25768 dchrptlem2 25769 disjex 30271 disjexc 30272 signsply0 31721 signstfveq0a 31746 bnj1177 32176 bnj1253 32187 fin2so 34761 br2coss 35565 stoweidlem36 42202 aovnuoveq 43271 aovovn0oveq 43274 ovn0dmfun 43878 rrx2pnedifcoorneor 44601 2itscp 44666 aacllem 44800 |
Copyright terms: Public domain | W3C validator |