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

Theorem eqtr2 2176
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 2159 . 2  |-  ( A  =  B  <->  B  =  A )
2 eqtr 2175 . 2  |-  ( ( B  =  A  /\  A  =  C )  ->  B  =  C )
31, 2sylanb 282 1  |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1335
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 1427  ax-gen 1429  ax-4 1490  ax-17 1506  ax-ext 2139
This theorem depends on definitions:  df-bi 116  df-cleq 2150
This theorem is referenced by:  eqvinc  2835  eqvincg  2836  moop2  4212  reusv3i  4420  relop  4737  f0rn0  5365  fliftfun  5747  th3qlem1  6583  enq0ref  7354  enq0tr  7355  genpdisj  7444  addlsub  8246  fsum2dlemstep  11335  0dvds  11711  cncongr1  11984
  Copyright terms: Public domain W3C validator