Theorem eqtr 2779

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2122  ax-ext 2730

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1783  df-cleq 2751

This theorem is referenced by:  eqtr2  2780  eqtr3  2781  sylan9eq  2814  eqvincg  3560  disjeq0  4353  uneqdifeq  4387  propeqop  5367  relresfld  6106  unixpid  6114  fvmptdf  6766  eqer  8335  xpider  8379  undifixp  8517  wemaplem2  9037  infeq5  9126  ficard  10018  winalim2  10149  addlsub  11087  pospo  17642  istos  17704  symg2bas  18581  dmatmul  21190  uhgr2edg  27090  clwlkclwwlkf1lem3  27883  eqtrb  30337  bnj545  32388  bnj934  32428  bnj953  32432  poseq  33349  soseq  33350  ordcmp  34178  bj-snmoore  34801  bj-isclm  34978  bj-bary1lem1  34998  poimirlem26  35356  heicant  35365  ismblfin  35371  volsupnfl  35375  itg2addnclem2  35382  itg2addnc  35384  rngodm1dm2  35643  rngoidmlem  35647  rngo1cl  35650  rngoueqz  35651  zerdivemp1x  35658  dvheveccl  38681  rp-isfinite5  40591  clcnvlem  40689  relexpxpmin  40784  gneispace  41203