Theorem eqtr2 2758

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Andrew Salmon, 25-May-2011.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)

Assertion

Ref	Expression
eqtr2	⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

Proof of Theorem eqtr2

Step	Hyp	Ref	Expression
1		eqeq1 2741	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpa 476	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:  eqvincg  3604  reusv3i  5351  moop2  5458  relopabi  5779  relop  5807  f0rn0  6727  fliftfun  7268  soseq  8111  addlsub  11565  wrd2ind  14658  fsum2dlem  15705  fprodser  15884  0dvds  16215  cncongr1  16606  4sqlem12  16896  cshwshashlem1  17035  catideu  17610  pj1eu  19637  lspsneu  21090  1marepvmarrepid  22531  mdetunilem6  22573  qtopeu  23672  qtophmeo  23773  dscmet  24528  isosctrlem2  26797  ppiub  27183  ltssolem1  27655  nolt02o  27675  nogt01o  27676  axcgrtr  29000  axeuclid  29048  axcontlem2  29050  uhgr2edg  29293  usgredgreu  29303  uspgredg2vtxeu  29305  wlkon2n0  29750  spthonepeq  29837  usgr2wlkneq  29841  2pthon3v  30028  umgr2adedgspth  30033  clwwlknondisj  30198  frgr2wwlkeqm  30418  2wspmdisj  30424  ajmoi  30946  chocunii  31389  3oalem2  31751  adjmo  31920  cdjreui  32520  eqtrb  32560  probun  34597  bnj551  34919  fineqvnttrclselem1  35299  satfv0fun  35587  satffunlem  35617  satffunlem1lem1  35618  satffunlem2lem1  35620  r1peuqusdeg1  35859  btwnswapid  36233  bj-snsetex  37211  bj-bary1lem1  37566  poimirlem4  37875  exidu1  38107  rngoideu  38154  disjimrmoeqec  39059  mapdpglem31  42079  grpods  42564  remul01  42777  frege55b  44253  frege55c  44274  cncfiooicclem1  46251  euoreqb  47469  isuspgrim0lem  48253  aacllem  50160