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 )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104   = wceq 1402

This proof depends on 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 proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqvinc  2949  eqvincg  2950  moop2  4392  reusv3i  4605  relop  4930  f0rn0  5587  fliftfun  6002  th3qlem1  6911  enq0ref  7801  enq0tr  7802  genpdisj  7891  addlsub  8698  wrd2ind  11511  fsum2dlemstep  12220  0dvds  12597  cncongr1  12900  4sqlem12  13204  ppiqub  16254  uhgr2edg  16613  usgredgreu  16623  uspgredg2vtxeu  16625