![]() |
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 2800 | . 2 ⊢ (𝐴 = 𝐶 ↔ 𝐵 = 𝐶) |
3 | 2 | necon3bii 3036 | 1 ⊢ (𝐴 ≠ 𝐶 ↔ 𝐵 ≠ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 207 = wceq 1522 ≠ wne 2984 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-9 2091 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-cleq 2788 df-ne 2985 |
This theorem is referenced by: eqnetri 3054 exss 5247 inisegn0 5837 suppvalbr 7685 brwitnlem 7983 en3lplem2 8922 hta 9172 kmlem3 9424 domtriomlem 9710 zorn2lem6 9769 konigthlem 9836 rpnnen1lem2 12226 rpnnen1lem1 12227 rpnnen1lem3 12228 rpnnen1lem5 12230 fsuppmapnn0fiubex 13210 seqf1olem1 13259 iscyg2 18724 gsumval3lem2 18747 opprirred 19142 ptclsg 21907 iscusp2 22594 dchrptlem1 25522 dchrptlem2 25523 disjex 30032 disjexc 30033 signsply0 31438 signstfveq0a 31463 bnj1177 31892 bnj1253 31903 fin2so 34429 br2coss 35233 stoweidlem36 41883 aovnuoveq 42926 aovovn0oveq 42929 ovn0dmfun 43533 rrx2pnedifcoorneor 44204 2itscp 44269 aacllem 44402 |
Copyright terms: Public domain | W3C validator |