Theorem eqtr3 2782

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  neneor  3057  moeq  3664  euind  3681  reuind  3710  disjeq0  4408  ssprsseq  4780  mosneq  4796  prnebg  4810  prnesn  4814  prel12g  4818  3elpr2eq  4833  eusv1  5353  axprglem  5394  xpcan  6170  xpcan2  6171  funopg  6579  funopdmsn  7159  funsndifnop  7160  fvf1pr  7319  resf1extb  7950  wfr3g  8345  oawordeulem  8570  nnasmo  8680  en1eqsn  9274  ixpfi2  9347  frr3g  9767  isf32lem2  10439  fpwwe2lem12  10734  1re  11315  receu  11968  xrlttri  13275  injresinjlem  13932  fsumparts  15982  odd2np1  16520  prmreclem2  17104  divsfval  17728  isprs  18479  psrn  18758  grpinveu  19194  symgextf1  19644  symgfixf1  19660  efgrelexlemb  19973  lspextmo  21340  evlseu  22401  tgcmp  23728  sqf11  27475  dchrisumlem2  27826  ltssolem1  28041  nocvxminlem  28149  divsmo  28579  axlowdimlem15  29543  axcontlem2  29552  wlksoneq1eq2  30252  spthonepeq  30347  uspgrn2crct  30406  wwlksnextinj  30497  frgrwopreglem5lem  30930  numclwwlk1lem2f1  30967  nsnlplig  31092  nsnlpligALT  31093  grpoinveu  31130  5oalem4  32268  rnbra  32718  xreceu  33538  bnj594  35592  bnj953  35619  ordunmax  35769  scottsn  35810  fnsingle  36805  funimage  36814  funtransport  36920  funray  37029  funline  37031  hilbert1.2  37044  lineintmo  37046  bj-bary1  38370  poimirlem13  38688  poimirlem14  38689  poimirlem17  38692  poimirlem27  38702  mopre  39540  sucmapleftuniq  39559  antisymressn  39603  disjdmqscossss  39975  prter2  40075  cdleme  41754  rediveud  43631  kelac2lem  44203  frege124d  44898  2ffzoeq  48534  sprsymrelf1lem  48709  paireqne  48729  usgrexmpl2trifr  49271  gpg5grlic  49328  pgnbgreunbgrlem2  49351  mof0ALT  50087  mofsn  50091  f1omoOLD  50144  oppcendc  50268  parhomidval  50882