Theorem eqtr 2782

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 2766	. 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 2734

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

This theorem is used by:  sylan9eq  2817  eqvincg  3605  disjeq0  4412  uneqdifeq  4451  propeqop  5488  relresfldOLD  6278  unixpid  6286  fvmptdf  6997  poseq  8159  soseq  8160  eqer  8736  xpider  8791  undifixp  8944  wemaplem2  9522  infeq5  9619  ficard  10576  winalim2  10708  addlsub  11657  pospo  18435  istos  18508  symg2bas  19521  dmatmul  22720  uhgr2edg  29654  clwlkclwwlkf1lem3  30462  eqtrb  32935  bnj545  35391  bnj934  35431  bnj953  35435  scottrankeqel  35618  ordcmp  37053  bj-snmoore  37850  bj-isclm  38030  bj-bary1lem1  38050  wl-dfcleq  38255  poimirlem26  38382  heicant  38391  ismblfin  38397  volsupnfl  38401  itg2addnclem2  38408  itg2addnc  38410  rngodm1dm2  38669  rngoidmlem  38673  rngo1cl  38676  rngoueqz  38677  zerdivemp1x  38684  disjdmqsss  39640  dvheveccl  41972  rp-isfinite5  44344  clcnvlem  44450  relexpxpmin  44544  gneispace  44961  resipos  49888