Theorem eqtr 2751

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  sylan9eq  2786  eqvincg  3598  disjeq0  4405  uneqdifeq  4442  propeqop  5450  relresfld  6229  unixpid  6237  fvmptdf  6941  poseq  8094  soseq  8095  eqer  8664  xpider  8718  undifixp  8864  wemaplem2  9439  infeq5  9533  ficard  10462  winalim2  10593  addlsub  11539  pospo  18255  istos  18328  symg2bas  19311  dmatmul  22418  uhgr2edg  29193  clwlkclwwlkf1lem3  29993  eqtrb  32460  bnj545  34914  bnj934  34954  bnj953  34958  ordcmp  36498  bj-snmoore  37164  bj-isclm  37342  bj-bary1lem1  37362  poimirlem26  37692  heicant  37701  ismblfin  37707  volsupnfl  37711  itg2addnclem2  37718  itg2addnc  37720  rngodm1dm2  37978  rngoidmlem  37982  rngo1cl  37985  rngoueqz  37986  zerdivemp1x  37993  disjdmqsss  38906  dvheveccl  41217  rp-isfinite5  43615  clcnvlem  43721  relexpxpmin  43815  gneispace  44232  resipos  49080