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

Theorem neeq1i 2752
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 2474 . 2  |-  ( A  =  C  <->  B  =  C )
32necon3bii 2735 1  |-  ( A  =/=  C  <->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1379    =/= wne 2662
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459  df-ne 2664
This theorem is referenced by:  neeq12iOLD  2757  eqnetri  2763  syl5eqnerOLD  2769  rabn0  3805  exss  4710  suppvalbr  6902  brwitnlem  7154  en3lplem2  8028  hta  8311  kmlem3  8528  domtriomlem  8818  zorn2lem6  8877  konigthlem  8939  rpnnen1lem1  11204  rpnnen1lem2  11205  rpnnen1lem3  11206  rpnnen1lem5  11208  fsuppmapnn0fiubex  12061  seqf1olem1  12109  iscyg2  16673  gsumval3lem2  16698  opprirred  17132  ptclsg  19848  iscusp2  20537  dchrptlem1  23264  dchrptlem2  23265  disjex  27121  disjexc  27122  eulerpartlems  27936  signsply0  28145  signstfveq0a  28170  fin2so  29614  inisegn0  30593  stoweidlem36  31336  aovnuoveq  31743  aovovn0oveq  31746  bnj1177  33141  bnj1253  33152
  Copyright terms: Public domain W3C validator