Theorem eqtr2 2790

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  eqvincg  3616  reusv3i  5373  moop2  5483  relopabi  5807  relop  5834  f0rn0  6761  fliftfun  7308  soseq  8151  addlsub  11626  wrd2ind  14756  fsum2dlem  15817  fprodser  15999  0dvds  16330  cncongr1  16721  4sqlem12  17012  cshwshashlem1  17151  catideu  17727  pj1eu  19762  lspsneu  21221  1marepvmarrepid  22697  mdetunilem6  22739  qtopeu  23838  qtophmeo  23939  dscmet  24694  isosctrlem2  26946  ppiub  27330  ltssolem1  27801  nolt02o  27821  nogt01o  27822  axcgrtr  29202  axeuclid  29250  axcontlem2  29252  uhgr2edg  29495  usgredgreu  29505  uspgredg2vtxeu  29507  wlkon2n0  29951  spthonepeq  30038  usgr2wlkneq  30042  2pthon3v  30229  umgr2adedgspth  30234  clwwlknondisj  30399  frgr2wwlkeqm  30619  2wspmdisj  30625  ajmoi  31147  chocunii  31590  3oalem2  31952  adjmo  32121  cdjreui  32721  eqtrb  32757  probun  34750  bnj551  35072  fineqvnttrclselem1  35453  satfv0fun  35758  satffunlem  35788  satffunlem1lem1  35789  satffunlem2lem1  35791  r1peuqusdeg1  36030  btwnswapid  36404  bj-snsetex  37483  bj-bary1lem1  37838  poimirlem4  38158  exidu1  38390  rngoideu  38437  disjimrmoeqec  39342  mapdpglem31  42362  grpods  42846  remul01  43053  frege55b  44510  frege55c  44531  cncfiooicclem1  46494  euoreqb  47730  isuspgrim0lem  48542  aacllem  50470