Theorem eqtr 2757

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 2741	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpar 477	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  sylan9eq  2792  eqvincg  3591  disjeq0  4397  uneqdifeq  4433  propeqop  5457  relresfld  6236  unixpid  6244  fvmptdf  6950  poseq  8103  soseq  8104  eqer  8675  xpider  8730  undifixp  8877  wemaplem2  9457  infeq5  9553  ficard  10482  winalim2  10614  addlsub  11561  pospo  18304  istos  18377  symg2bas  19363  dmatmul  22476  uhgr2edg  29295  clwlkclwwlkf1lem3  30095  eqtrb  32562  bnj545  35057  bnj934  35097  bnj953  35101  ordcmp  36649  bj-snmoore  37445  bj-isclm  37625  bj-bary1lem1  37645  wl-dfcleq  37850  poimirlem26  37987  heicant  37996  ismblfin  38002  volsupnfl  38006  itg2addnclem2  38013  itg2addnc  38015  rngodm1dm2  38273  rngoidmlem  38277  rngo1cl  38280  rngoueqz  38281  zerdivemp1x  38288  disjdmqsss  39246  dvheveccl  41578  rp-isfinite5  43968  clcnvlem  44074  relexpxpmin  44168  gneispace  44585  resipos  49468