MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  neeq1i Structured version   Unicode version

Theorem neeq1i 2688
Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.) (Proof shortened by Wolf Lammen, 19-Nov-2019.)
Hypothesis
Ref Expression
neeq1i.1  |-  A  =  B
Assertion
Ref Expression
neeq1i  |-  ( A  =/=  C  <->  B  =/=  C )

Proof of Theorem neeq1i
StepHypRef Expression
1 neeq1i.1 . . 3  |-  A  =  B
21eqeq1i 2409 . 2  |-  ( A  =  C  <->  B  =  C )
32necon3bii 2671 1  |-  ( A  =/=  C  <->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1405    =/= wne 2598
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-cleq 2394  df-ne 2600
This theorem is referenced by:  neeq12iOLD  2693  eqnetri  2699  syl5eqnerOLD  2705  rabn0  3758  exss  4653  suppvalbr  6860  brwitnlem  7114  en3lplem2  7985  hta  8267  kmlem3  8484  domtriomlem  8774  zorn2lem6  8833  konigthlem  8895  rpnnen1lem1  11171  rpnnen1lem2  11172  rpnnen1lem3  11173  rpnnen1lem5  11175  fsuppmapnn0fiubex  12052  seqf1olem1  12100  iscyg2  17101  gsumval3lem2  17126  opprirred  17563  ptclsg  20300  iscusp2  20989  dchrptlem1  23812  dchrptlem2  23813  disjex  27764  disjexc  27765  signsply0  28894  signstfveq0a  28919  bnj1177  29270  bnj1253  29281  fin2so  31393  inisegn0  35332  stoweidlem36  37168  aovnuoveq  37626  aovovn0oveq  37629  ovn0dmfun  38061  aacllem  38840
  Copyright terms: Public domain W3C validator