Theorem eqtr3 2763

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

Assertion

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

Proof of Theorem eqtr3

Step	Hyp	Ref	Expression
1		eqeq2 2749	. 2 ⊢ (𝐵 = 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
2	1	biimparc 483	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1788  df-cleq 2729

This theorem is referenced by:  neneor  3041  moeq  3620  euind  3637  reuind  3666  disjeq0  4370  ssprsseq  4738  mosneq  4753  prnebg  4766  prnesn  4770  prel12g  4774  3elpr2eq  4818  eusv1  5284  xpcan  6039  xpcan2  6040  funopg  6414  funopdmsn  6965  funsndifnop  6966  mpofunOLD  7335  wfr3g  8053  oawordeulem  8282  ixpfi2  8974  frr3g  9372  isf32lem2  9968  fpwwe2lem12  10256  1re  10833  receu  11477  xrlttri  12729  injresinjlem  13362  cshwsexa  14389  fsumparts  15370  odd2np1  15902  prmreclem2  16470  divsfval  17052  isprs  17804  psrn  18081  grpinveu  18402  symgextf1  18813  symgfixf1  18829  efgrelexlemb  19140  lspextmo  20093  evlseu  21043  tgcmp  22298  sqf11  26021  dchrisumlem2  26371  axlowdimlem15  27047  axcontlem2  27056  wlksoneq1eq2  27752  spthonepeq  27839  uspgrn2crct  27892  wwlksnextinj  27983  frgrwopreglem5lem  28403  numclwwlk1lem2f1  28440  nsnlplig  28562  nsnlpligALT  28563  grpoinveu  28600  5oalem4  29738  rnbra  30188  xreceu  30916  bnj594  32605  bnj953  32632  nnasmo  33409  sltsolem1  33615  nocvxminlem  33709  fnsingle  33958  funimage  33967  funtransport  34070  funray  34179  funline  34181  hilbert1.2  34194  lineintmo  34196  bj-bary1  35217  poimirlem13  35527  poimirlem14  35528  poimirlem17  35531  poimirlem27  35541  prter2  36632  cdleme  38311  kelac2lem  40592  frege124d  41046  2ffzoeq  44493  sprsymrelf1lem  44616  paireqne  44636  mof0ALT  45840  mofsn  45844  f1omo  45861