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

Theorem eqtr2 2106
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Assertion
Ref Expression
eqtr2  |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )

Proof of Theorem eqtr2
StepHypRef Expression
1 eqcom 2090 . 2  |-  ( A  =  B  <->  B  =  A )
2 eqtr 2105 . 2  |-  ( ( B  =  A  /\  A  =  C )  ->  B  =  C )
31, 2sylanb 278 1  |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )
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:  eqvinc  2740  eqvincg  2741  moop2  4078  reusv3i  4281  relop  4586  f0rn0  5205  fliftfun  5575  th3qlem1  6394  enq0ref  6992  enq0tr  6993  genpdisj  7082  addlsub  7848  fsum2dlemstep  10828  0dvds  11094  cncongr1  11363
  Copyright terms: Public domain W3C validator