Theorem eqtr3 2751

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  neneor  3025  moeq  3667  euind  3684  reuind  3713  disjeq0  4407  ssprsseq  4776  mosneq  4793  prnebg  4807  prnesn  4811  prel12g  4815  3elpr2eq  4857  eusv1  5330  xpcan  6125  xpcan2  6126  funopg  6516  funopdmsn  7084  funsndifnop  7085  fvf1pr  7244  resf1extb  7867  wfr3g  8252  oawordeulem  8472  nnasmo  8581  en1eqsn  9164  ixpfi2  9240  frr3g  9652  isf32lem2  10248  fpwwe2lem12  10536  1re  11115  receu  11765  xrlttri  13041  injresinjlem  13690  cshwsexaOLD  14731  fsumparts  15713  odd2np1  16252  prmreclem2  16829  divsfval  17451  isprs  18202  psrn  18481  grpinveu  18853  symgextf1  19300  symgfixf1  19316  efgrelexlemb  19629  lspextmo  20960  evlseu  21988  tgcmp  23286  sqf11  27047  dchrisumlem2  27399  sltsolem1  27585  nocvxminlem  27688  divsmo  28092  axlowdimlem15  28901  axcontlem2  28910  wlksoneq1eq2  29608  spthonepeq  29697  uspgrn2crct  29753  wwlksnextinj  29844  frgrwopreglem5lem  30264  numclwwlk1lem2f1  30301  nsnlplig  30425  nsnlpligALT  30426  grpoinveu  30463  5oalem4  31601  rnbra  32051  xreceu  32862  bnj594  34879  bnj953  34906  fnsingle  35893  funimage  35902  funtransport  36005  funray  36114  funline  36116  hilbert1.2  36129  lineintmo  36131  bj-bary1  37286  poimirlem13  37613  poimirlem14  37614  poimirlem17  37617  poimirlem27  37627  antisymressn  38421  disjdmqscossss  38781  prter2  38860  cdleme  40539  rediveud  42416  kelac2lem  43037  frege124d  43734  2ffzoeq  47311  sprsymrelf1lem  47475  paireqne  47495  usgrexmpl2trifr  48021  gpg5grlic  48078  pgnbgreunbgrlem2  48101  mof0ALT  48824  mofsn  48828  f1omoOLD  48878  oppcendc  49003