Theorem eqtr2 2257

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 2240	. 2 |- ( A = B <-> B = A )
2		eqtr 2256	. 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 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqvinc  2949  eqvincg  2950  moop2  4387  reusv3i  4600  relop  4925  f0rn0  5582  fliftfun  5992  th3qlem1  6901  enq0ref  7790  enq0tr  7791  genpdisj  7880  addlsub  8686  wrd2ind  11473  fsum2dlemstep  12179  0dvds  12556  cncongr1  12859  4sqlem12  13159  uhgr2edg  16361  usgredgreu  16371  uspgredg2vtxeu  16373