Theorem eqtr 2780

Description: Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)

Assertion

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

Proof of Theorem eqtr

Step	Hyp	Ref	Expression
1		eqeq1 2764	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpar 483	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752

This theorem is used by:  sylan9eq  2815  eqvincg  3602  disjeq0  4409  uneqdifeq  4448  propeqop  5477  relresfldOLD  6269  unixpid  6277  fvmptdf  6989  poseq  8154  soseq  8155  eqer  8733  xpider  8788  undifixp  8941  wemaplem2  9519  infeq5  9616  ficard  10606  winalim2  10738  addlsub  11687  pospo  18464  istos  18537  symg2bas  19554  dmatmul  22759  uhgr2edg  29708  clwlkclwwlkf1lem3  30516  eqtrb  32989  bnj545  35445  bnj934  35485  bnj953  35489  scottrankeqel  35672  ordcmp  37151  bj-snmoore  37948  bj-isclm  38126  bj-bary1lem1  38146  wl-dfcleq  38351  poimirlem26  38478  heicant  38487  ismblfin  38493  volsupnfl  38497  itg2addnclem2  38504  itg2addnc  38506  rngodm1dm2  38780  rngoidmlem  38784  rngo1cl  38787  rngoueqz  38788  zerdivemp1x  38795  disjdmqsss  39751  dvheveccl  42083  rp-isfinite5  44455  clcnvlem  44561  relexpxpmin  44655  gneispace  45072  resipos  49999