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

Theorem neeq1i 2553
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 2551 . 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 177    = wceq 1649    =/= wne 2543
This theorem is referenced by:  neeq12i  2555  eqnetri  2560  syl5eqner  2568  rabn0  3583  exss  4360  brwitnlem  6680  en3lplem2  7597  hta  7747  kmlem3  7958  domtriomlem  8248  zorn2lem6  8307  konigthlem  8369  rpnnen1lem1  10525  rpnnen1lem2  10526  rpnnen1lem3  10527  rpnnen1lem5  10529  seqf1olem1  11282  iscyg2  15412  opprirred  15727  ptclsg  17561  iscusp2  18246  dchrptlem1  20908  dchrptlem2  20909  disjex  23868  disjexc  23869  inisegn0  26802  stoweidlem36  27446  aovnuoveq  27717  aovovn0oveq  27720  bnj1177  28706  bnj1253  28717
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2373  df-ne 2545
  Copyright terms: Public domain W3C validator