Theorem eqtr3 2766

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  neneor  3048  moeq  3729  euind  3746  reuind  3775  disjeq0  4479  ssprsseq  4850  mosneq  4867  prnebg  4880  prnesn  4884  prel12g  4888  3elpr2eq  4930  eusv1  5409  xpcan  6207  xpcan2  6208  funopg  6612  funopdmsn  7184  funsndifnop  7185  fvf1pr  7343  wfr3g  8363  oawordeulem  8610  nnasmo  8719  en1eqsn  9336  ixpfi2  9420  frr3g  9825  isf32lem2  10423  fpwwe2lem12  10711  1re  11290  receu  11935  xrlttri  13201  injresinjlem  13837  cshwsexaOLD  14873  fsumparts  15854  odd2np1  16389  prmreclem2  16964  divsfval  17607  isprs  18367  psrn  18645  grpinveu  19014  symgextf1  19463  symgfixf1  19479  efgrelexlemb  19792  lspextmo  21078  evlseu  22130  tgcmp  23430  sqf11  27200  dchrisumlem2  27552  sltsolem1  27738  nocvxminlem  27840  divsmo  28228  axlowdimlem15  28989  axcontlem2  28998  wlksoneq1eq2  29700  spthonepeq  29788  uspgrn2crct  29841  wwlksnextinj  29932  frgrwopreglem5lem  30352  numclwwlk1lem2f1  30389  nsnlplig  30513  nsnlpligALT  30514  grpoinveu  30551  5oalem4  31689  rnbra  32139  xreceu  32886  bnj594  34888  bnj953  34915  fnsingle  35883  funimage  35892  funtransport  35995  funray  36104  funline  36106  hilbert1.2  36119  lineintmo  36121  bj-bary1  37278  poimirlem13  37593  poimirlem14  37594  poimirlem17  37597  poimirlem27  37607  antisymressn  38400  disjdmqscossss  38759  prter2  38837  cdleme  40517  kelac2lem  43021  frege124d  43723  2ffzoeq  47242  sprsymrelf1lem  47365  paireqne  47385  usgrexmpl2trifr  47852  mof0ALT  48553  mofsn  48557  f1omo  48574