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

Theorem eqtr3 2101
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 2084 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2099 . 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 1285
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 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  eueq  2764  euind  2780  reuind  2796  preqsn  3575  eusv1  4210  funopg  4964  funinsn  4979  foco  5147  mpt2fun  5634  enq0tr  6686  lteupri  6869  elrealeu  7060  rereceu  7117  receuap  7826  xrltso  8947  xrlttri3  8948  odd2np1  10417
  Copyright terms: Public domain W3C validator