Theorem eqtr3 2759

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 479	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  neneor  3033  moeq  3654  euind  3671  reuind  3700  disjeq0  4397  ssprsseq  4769  mosneq  4786  prnebg  4800  prnesn  4804  prel12g  4808  3elpr2eq  4850  eusv1  5329  axprglem  5374  xpcan  6135  xpcan2  6136  funopg  6527  funopdmsn  7098  funsndifnop  7099  fvf1pr  7256  resf1extb  7879  wfr3g  8263  oawordeulem  8483  nnasmo  8593  en1eqsn  9179  ixpfi2  9254  frr3g  9674  isf32lem2  10270  fpwwe2lem12  10559  1re  11138  receu  11789  xrlttri  13084  injresinjlem  13739  fsumparts  15763  odd2np1  16304  prmreclem2  16882  divsfval  17505  isprs  18256  psrn  18535  grpinveu  18944  symgextf1  19390  symgfixf1  19406  efgrelexlemb  19719  lspextmo  21046  evlseu  22074  tgcmp  23379  sqf11  27119  dchrisumlem2  27470  ltssolem1  27656  nocvxminlem  27763  divsmo  28193  axlowdimlem15  29042  axcontlem2  29051  wlksoneq1eq2  29749  spthonepeq  29838  uspgrn2crct  29894  wwlksnextinj  29985  frgrwopreglem5lem  30408  numclwwlk1lem2f1  30445  nsnlplig  30570  nsnlpligALT  30571  grpoinveu  30608  5oalem4  31746  rnbra  32196  xreceu  32999  bnj594  35073  bnj953  35100  fnsingle  36118  funimage  36127  funtransport  36232  funray  36341  funline  36343  hilbert1.2  36356  lineintmo  36358  bj-bary1  37645  poimirlem13  37971  poimirlem14  37972  poimirlem17  37975  poimirlem27  37985  mopre  38809  sucmapleftuniq  38828  antisymressn  38872  disjdmqscossss  39244  prter2  39344  cdleme  41023  rediveud  42892  kelac2lem  43513  frege124d  44209  2ffzoeq  47791  sprsymrelf1lem  47966  paireqne  47986  usgrexmpl2trifr  48528  gpg5grlic  48585  pgnbgreunbgrlem2  48608  mof0ALT  49330  mofsn  49334  f1omoOLD  49384  oppcendc  49508