Theorem eqtr2 2784

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 2767	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 = 𝐶 ↔ 𝐵 = 𝐶))
2	1	biimpa 481	1 ⊢ ((𝐴 = 𝐵 ∧ 𝐴 = 𝐶) → 𝐵 = 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  eqvincg  3607  reusv3i  5375  moop2  5485  relopabi  5809  relop  5836  f0rn0  6763  fliftfun  7310  soseq  8151  addlsub  11625  wrd2ind  14756  fsum2dlem  15817  fprodser  15999  0dvds  16329  cncongr1  16720  4sqlem12  17011  cshwshashlem1  17150  catideu  17726  pj1eu  19761  lspsneu  21247  1marepvmarrepid  22732  mdetunilem6  22774  qtopeu  23873  qtophmeo  23974  dscmet  24729  isosctrlem2  26984  ppiub  27368  ltssolem1  27839  nolt02o  27859  nogt01o  27860  axcgrtr  29265  axeuclid  29313  axcontlem2  29315  uhgr2edg  29558  usgredgreu  29568  uspgredg2vtxeu  29570  wlkon2n0  30014  spthonepeq  30101  usgr2wlkneq  30105  2pthon3v  30292  umgr2adedgspth  30297  clwwlknondisj  30462  frgr2wwlkeqm  30682  2wspmdisj  30688  ajmoi  31210  chocunii  31653  3oalem2  32015  adjmo  32184  cdjreui  32784  eqtrb  32820  probun  34809  bnj551  35131  fineqvnttrclselem1  35534  satfv0fun  35863  satffunlem  35893  satffunlem1lem1  35894  satffunlem2lem1  35896  r1peuqusdeg1  36135  btwnswapid  36509  bj-snsetex  37599  bj-bary1lem1  37955  poimirlem4  38275  exidu1  38507  rngoideu  38554  disjimrmoeqec  39457  mapdpglem31  42477  grpods  42961  remul01  43168  frege55b  44623  frege55c  44644  cncfiooicclem1  46607  euoreqb  47846  isuspgrim0lem  48658  aacllem  50621