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

Theorem neeq1i 2728
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 2450 . 2  |-  ( A  =  C  <->  B  =  C )
32necon3bii 2711 1  |-  ( A  =/=  C  <->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    = wceq 1383    =/= wne 2638
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435  df-ne 2640
This theorem is referenced by:  neeq12iOLD  2733  eqnetri  2739  syl5eqnerOLD  2745  rabn0  3791  exss  4700  suppvalbr  6907  brwitnlem  7159  en3lplem2  8035  hta  8318  kmlem3  8535  domtriomlem  8825  zorn2lem6  8884  konigthlem  8946  rpnnen1lem1  11219  rpnnen1lem2  11220  rpnnen1lem3  11221  rpnnen1lem5  11223  fsuppmapnn0fiubex  12080  seqf1olem1  12128  iscyg2  16864  gsumval3lem2  16889  opprirred  17330  ptclsg  20094  iscusp2  20783  dchrptlem1  23517  dchrptlem2  23518  disjex  27429  disjexc  27430  signsply0  28486  signstfveq0a  28511  fin2so  30016  inisegn0  30965  stoweidlem36  31772  aovnuoveq  32230  aovovn0oveq  32233  ovn0dmfun  32406  bnj1177  33930  bnj1253  33941
  Copyright terms: Public domain W3C validator