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

Theorem neeq1i 2469
Description: Inference for inequality. (Contributed by NM, 29-Apr-2005.)
Hypothesis
Ref Expression
neeq1i.1  |-  A  =  B
Assertion
Ref Expression
neeq1i  |-  ( A  =/=  C  <->  B  =/=  C )

Proof of Theorem neeq1i
StepHypRef Expression
1 neeq1i.1 . 2  |-  A  =  B
2 neeq1 2467 . 2  |-  ( A  =  B  ->  ( A  =/=  C  <->  B  =/=  C ) )
31, 2ax-mp 8 1  |-  ( A  =/=  C  <->  B  =/=  C )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    = wceq 1632    =/= wne 2459
This theorem is referenced by:  neeq12i  2471  eqnetri  2476  syl5eqner  2484  rabn0  3487  exss  4252  brwitnlem  6522  en3lplem2  7433  hta  7583  kmlem3  7794  domtriomlem  8084  zorn2lem6  8144  konigthlem  8206  rpnnen1lem1  10358  rpnnen1lem2  10359  rpnnen1lem3  10360  rpnnen1lem5  10362  seqf1olem1  11101  iscyg2  15185  opprirred  15500  ptclsg  17325  dchrptlem1  20519  dchrptlem2  20520  nbssntrs  26250  inisegn0  27243  stoweidlem36  27888  aovnuoveq  28159  aovovn0oveq  28162  bnj1177  29352  bnj1253  29363
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289  df-ne 2461
  Copyright terms: Public domain W3C validator