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

Theorem neeq1i 2690
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 2458 . 2  |-  ( A  =  C  <->  B  =  C )
32necon3bii 2678 1  |-  ( A  =/=  C  <->  B  =/=  C )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    = wceq 1446    =/= wne 2624
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-ext 2433
This theorem depends on definitions:  df-bi 189  df-cleq 2446  df-ne 2626
This theorem is referenced by:  eqnetri  2696  rabn0  3754  exss  4666  inisegn0  5203  suppvalbr  6923  brwitnlem  7214  en3lplem2  8125  hta  8373  kmlem3  8587  domtriomlem  8877  zorn2lem6  8936  konigthlem  8998  rpnnen1lem1  11297  rpnnen1lem2  11298  rpnnen1lem3  11299  rpnnen1lem5  11301  fsuppmapnn0fiubex  12211  seqf1olem1  12259  iscyg2  17529  gsumval3lem2  17552  opprirred  17942  ptclsg  20642  iscusp2  21329  dchrptlem1  24204  dchrptlem2  24205  disjex  28214  disjexc  28215  signsply0  29452  signstfveq0a  29477  bnj1177  29827  bnj1253  29838  fin2so  31944  stoweidlem36  37907  aovnuoveq  38703  aovovn0oveq  38706  ovn0dmfun  39868  aacllem  40644
  Copyright terms: Public domain W3C validator