Theorem eqtr3 2157

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 2139	. 2 |- ( B = C <-> C = B )
2		eqtr 2155	. 2 |- ( ( A = C /\ C = B ) -> A = B )
3	1, 2	sylan2b 285	1 |- ( ( A = C /\ B = C ) -> A = B )

Syntax hints:   -> wi 4   /\ wa 103   = wceq 1331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-cleq 2130

This theorem is referenced by:  eueq  2850  euind  2866  reuind  2884  preqsn  3697  eusv1  4368  funopg  5152  funinsn  5167  foco  5350  mpofun  5866  enq0tr  7235  lteupri  7418  elrealeu  7630  rereceu  7690  receuap  8423  xrltso  9575  xrlttri3  9576  iseqf1olemab  10255  fsumparts  11232  odd2np1  11559  exmidsbthrlem  13206