Theorem eqtr3 2258

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

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:  eueq  2997  euind  3013  reuind  3031  ssprsseq  3877  preqsn  3900  eusv1  4598  funopg  5411  funinsn  5430  foco  5626  funopdmsn  5895  mpofun  6190  enq0tr  7802  lteupri  7985  elrealeu  8197  rereceu  8257  receuap  9002  xrltso  10209  xrlttri3  10210  iseqf1olemab  10954  fsumparts  12256  odd2np1  12659  grpinveu  13896  exmidsbthrlem  17233