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

Theorem eqtr3 2135
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 2117 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2133 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 283 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1314
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  eueq  2826  euind  2842  reuind  2860  preqsn  3670  eusv1  4341  funopg  5125  funinsn  5140  foco  5323  mpofun  5839  enq0tr  7206  lteupri  7389  elrealeu  7601  rereceu  7661  receuap  8390  xrltso  9522  xrlttri3  9523  iseqf1olemab  10202  fsumparts  11179  odd2np1  11466  exmidsbthrlem  13019
  Copyright terms: Public domain W3C validator