Theorem eqtr2 2257

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 2240	. 2 ⊢ (𝐴 = 𝐵 ↔ 𝐵 = 𝐴)
2		eqtr 2256	. 2 ⊢ ((𝐵 = 𝐴 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)
3	1, 2	sylanb 284	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:  eqvinc  2949  eqvincg  2950  moop2  4394  reusv3i  4607  relop  4932  f0rn0  5590  fliftfun  6005  th3qlem1  6915  enq0ref  7806  enq0tr  7807  genpdisj  7896  addlsub  8703  wrd2ind  11517  fsum2dlemstep  12226  0dvds  12603  cncongr1  12906  4sqlem12  13210  ppiqub  16293  uhgr2edg  16652  usgredgreu  16662  uspgredg2vtxeu  16664  idjudju  17252