Theorem eqtr3 2764

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 2750	. 2 ⊢ (𝐵 = 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
2	1	biimparc 479	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  neneor  3043  moeq  3637  euind  3654  reuind  3683  disjeq0  4386  ssprsseq  4755  mosneq  4770  prnebg  4783  prnesn  4787  prel12g  4791  3elpr2eq  4835  eusv1  5309  xpcan  6068  xpcan2  6069  funopg  6452  funopdmsn  7004  funsndifnop  7005  mpofunOLD  7377  wfr3g  8109  oawordeulem  8347  ixpfi2  9047  frr3g  9445  isf32lem2  10041  fpwwe2lem12  10329  1re  10906  receu  11550  xrlttri  12802  injresinjlem  13435  cshwsexa  14465  fsumparts  15446  odd2np1  15978  prmreclem2  16546  divsfval  17175  isprs  17930  psrn  18208  grpinveu  18529  symgextf1  18944  symgfixf1  18960  efgrelexlemb  19271  lspextmo  20233  evlseu  21203  tgcmp  22460  sqf11  26193  dchrisumlem2  26543  axlowdimlem15  27227  axcontlem2  27236  wlksoneq1eq2  27934  spthonepeq  28021  uspgrn2crct  28074  wwlksnextinj  28165  frgrwopreglem5lem  28585  numclwwlk1lem2f1  28622  nsnlplig  28744  nsnlpligALT  28745  grpoinveu  28782  5oalem4  29920  rnbra  30370  xreceu  31098  bnj594  32792  bnj953  32819  nnasmo  33596  sltsolem1  33805  nocvxminlem  33899  fnsingle  34148  funimage  34157  funtransport  34260  funray  34369  funline  34371  hilbert1.2  34384  lineintmo  34386  bj-bary1  35410  poimirlem13  35717  poimirlem14  35718  poimirlem17  35721  poimirlem27  35731  prter2  36822  cdleme  38501  kelac2lem  40805  frege124d  41258  2ffzoeq  44708  sprsymrelf1lem  44831  paireqne  44851  mof0ALT  46055  mofsn  46059  f1omo  46076