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  3604  disjeq0  4410  uneqdifeq  4447  propeqop  5465  relresfld  6244  unixpid  6252  fvmptdf  6958  poseq  8112  soseq  8113  eqer  8684  xpider  8739  undifixp  8886  wemaplem2  9466  infeq5  9560  ficard  10489  winalim2  10621  addlsub  11567  pospo  18280  istos  18353  symg2bas  19339  dmatmul  22458  uhgr2edg  29299  clwlkclwwlkf1lem3  30099  eqtrb  32566  bnj545  35077  bnj934  35117  bnj953  35121  ordcmp  36669  bj-snmoore  37393  bj-isclm  37573  bj-bary1lem1  37593  poimirlem26  37926  heicant  37935  ismblfin  37941  volsupnfl  37945  itg2addnclem2  37952  itg2addnc  37954  rngodm1dm2  38212  rngoidmlem  38216  rngo1cl  38219  rngoueqz  38220  zerdivemp1x  38227  disjdmqsss  39185  dvheveccl  41517  rp-isfinite5  43902  clcnvlem  44008  relexpxpmin  44102  gneispace  44519  resipos  49363