Theorem eqtr3 2119

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

Assertion

Ref	Expression
eqtr3	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

Proof of Theorem eqtr3

Step	Hyp	Ref	Expression
1		eqcom 2102	. 2 ⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵)
2		eqtr 2117	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐵) → 𝐴 = 𝐵)
3	1, 2	sylan2b 283	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 103   = wceq 1299

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-gen 1393  ax-4 1455  ax-17 1474  ax-ext 2082

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

This theorem is referenced by:  eueq  2808  euind  2824  reuind  2842  preqsn  3649  eusv1  4311  funopg  5093  funinsn  5108  foco  5291  mpofun  5805  enq0tr  7143  lteupri  7326  elrealeu  7517  rereceu  7574  receuap  8291  xrltso  9423  xrlttri3  9424  iseqf1olemab  10103  fsumparts  11078  odd2np1  11365  exmidsbthrlem  12801