Theorem eqtr3 2252

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 2234	. 2 ⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵)
2		eqtr 2250	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐵) → 𝐴 = 𝐵)
3	1, 2	sylan2b 287	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 104   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  eueq  2988  euind  3004  reuind  3022  ssprsseq  3856  preqsn  3879  eusv1  4573  funopg  5386  funinsn  5405  foco  5601  funopdmsn  5864  mpofun  6155  enq0tr  7749  lteupri  7932  elrealeu  8144  rereceu  8204  receuap  8943  xrltso  10129  xrlttri3  10130  iseqf1olemab  10864  fsumparts  12156  odd2np1  12559  grpinveu  13751  exmidsbthrlem  16802