Theorem eqtr2 2225

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Assertion

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

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqcom 2208	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2		eqtr 2224	. 2 ⊢ ((𝐵 = 𝐴 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)
3	1, 2	sylanb 284	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

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

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqvinc  2900  eqvincg  2901  moop2  4304  reusv3i  4514  relop  4836  f0rn0  5482  fliftfun  5878  th3qlem1  6737  enq0ref  7566  enq0tr  7567  genpdisj  7656  addlsub  8462  wrd2ind  11199  fsum2dlemstep  11820  0dvds  12197  cncongr1  12500  4sqlem12  12800