Theorem eqtr2 2226

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

Step	Hyp	Ref	Expression
1		eqcom 2209	. 2 |- ( A = B <-> B = A )
2		eqtr 2225	. 2 |- ( ( B = A /\ A = C ) -> B = C )
3	1, 2	sylanb 284	1 |- ( ( A = B /\ A = C ) -> B = C )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-cleq 2200

This theorem is referenced by:  eqvinc  2903  eqvincg  2904  moop2  4314  reusv3i  4524  relop  4846  f0rn0  5492  fliftfun  5888  th3qlem1  6747  enq0ref  7581  enq0tr  7582  genpdisj  7671  addlsub  8477  wrd2ind  11214  fsum2dlemstep  11860  0dvds  12237  cncongr1  12540  4sqlem12  12840