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

Theorem eqtr2 2196
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 2179 . 2  |-  ( A  =  B  <->  B  =  A )
2 eqtr 2195 . 2  |-  ( ( B  =  A  /\  A  =  C )  ->  B  =  C )
31, 2sylanb 284 1  |-  ( ( A  =  B  /\  A  =  C )  ->  B  =  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    = wceq 1353
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  eqvinc  2860  eqvincg  2861  moop2  4251  reusv3i  4459  relop  4777  f0rn0  5410  fliftfun  5796  th3qlem1  6636  enq0ref  7431  enq0tr  7432  genpdisj  7521  addlsub  8326  fsum2dlemstep  11441  0dvds  11817  cncongr1  12102
  Copyright terms: Public domain W3C validator