Theorem eqtr3 2197

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.)

Assertion

Ref	Expression
eqtr3	|- ( ( A = C /\ B = C ) -> A = B )

Proof of Theorem eqtr3

Step	Hyp	Ref	Expression
1		eqcom 2179	. 2 |- ( B = C <-> C = B )
2		eqtr 2195	. 2 |- ( ( A = C /\ C = B ) -> A = B )
3	1, 2	sylan2b 287	1 |- ( ( A = C /\ B = C ) -> A = B )

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:  eueq  2908  euind  2924  reuind  2942  preqsn  3774  eusv1  4450  funopg  5247  funinsn  5262  foco  5445  mpofun  5972  enq0tr  7428  lteupri  7611  elrealeu  7823  rereceu  7883  receuap  8620  xrltso  9790  xrlttri3  9791  iseqf1olemab  10482  fsumparts  11469  odd2np1  11868  grpinveu  12839  exmidsbthrlem  14541