Theorem eqtr3 2761

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  neneor  3034  moeq  3648  euind  3665  reuind  3694  disjeq0  4384  ssprsseq  4756  mosneq  4773  prnebg  4787  prnesn  4791  prel12g  4795  3elpr2eq  4837  eusv1  5320  axprglem  5365  xpcan  6127  xpcan2  6128  funopg  6519  funopdmsn  7093  funsndifnop  7094  fvf1pr  7251  resf1extb  7874  wfr3g  8259  oawordeulem  8479  nnasmo  8589  en1eqsn  9175  ixpfi2  9250  frr3g  9671  isf32lem2  10267  fpwwe2lem12  10556  1re  11135  receu  11786  xrlttri  13081  injresinjlem  13736  fsumparts  15760  odd2np1  16301  prmreclem2  16879  divsfval  17502  isprs  18253  psrn  18532  grpinveu  18941  symgextf1  19387  symgfixf1  19403  efgrelexlemb  19716  lspextmo  21046  evlseu  22059  tgcmp  23384  sqf11  27120  dchrisumlem2  27471  ltssolem1  27657  nocvxminlem  27764  divsmo  28194  axlowdimlem15  29043  axcontlem2  29052  wlksoneq1eq2  29749  spthonepeq  29838  uspgrn2crct  29894  wwlksnextinj  29985  frgrwopreglem5lem  30408  numclwwlk1lem2f1  30445  nsnlplig  30570  nsnlpligALT  30571  grpoinveu  30608  5oalem4  31746  rnbra  32196  xreceu  33000  bnj594  35094  bnj953  35121  fnsingle  36145  funimage  36154  funtransport  36259  funray  36368  funline  36370  hilbert1.2  36383  lineintmo  36385  bj-bary1  37672  poimirlem13  38000  poimirlem14  38001  poimirlem17  38004  poimirlem27  38014  mopre  38838  sucmapleftuniq  38857  antisymressn  38901  disjdmqscossss  39273  prter2  39373  cdleme  41052  rediveud  42920  kelac2lem  43509  frege124d  44205  2ffzoeq  47791  sprsymrelf1lem  47966  paireqne  47986  usgrexmpl2trifr  48528  gpg5grlic  48585  pgnbgreunbgrlem2  48608  mof0ALT  49330  mofsn  49334  f1omoOLD  49384  oppcendc  49508