ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqtr3 Unicode version

Theorem eqtr3 2107
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.)
Assertion
Ref Expression
eqtr3  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )

Proof of Theorem eqtr3
StepHypRef Expression
1 eqcom 2090 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2105 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 281 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1289
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  eueq  2786  euind  2802  reuind  2820  preqsn  3619  eusv1  4274  funopg  5048  funinsn  5063  foco  5243  mpt2fun  5747  enq0tr  6993  lteupri  7176  elrealeu  7367  rereceu  7424  receuap  8138  xrltso  9266  xrlttri3  9267  iseqf1olemab  9918  fsumparts  10864  odd2np1  11151  exmidsbthrlem  11912
  Copyright terms: Public domain W3C validator