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 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  neneor  3057  moeq  3665  euind  3682  reuind  3711  disjeq0  4409  ssprsseq  4786  mosneq  4802  prnebg  4816  prnesn  4820  prel12g  4824  3elpr2eq  4866  eusv1  5356  axprglem  5401  xpcan  6169  xpcan2  6170  funopg  6568  funopdmsn  7148  funsndifnop  7149  fvf1pr  7309  resf1extb  7932  wfr3g  8319  oawordeulem  8542  nnasmo  8652  en1eqsn  9246  ixpfi2  9318  frr3g  9739  isf32lem2  10357  fpwwe2lem12  10652  1re  11233  receu  11884  xrlttri  13191  injresinjlem  13847  fsumparts  15894  odd2np1  16432  prmreclem2  17010  divsfval  17634  isprs  18385  psrn  18664  grpinveu  19099  symgextf1  19549  symgfixf1  19565  efgrelexlemb  19878  lspextmo  21241  evlseu  22300  tgcmp  23627  sqf11  27376  dchrisumlem2  27727  ltssolem1  27912  nocvxminlem  28020  divsmo  28450  axlowdimlem15  29414  axcontlem2  29423  wlksoneq1eq2  30123  spthonepeq  30218  uspgrn2crct  30277  wwlksnextinj  30368  frgrwopreglem5lem  30801  numclwwlk1lem2f1  30838  nsnlplig  30963  nsnlpligALT  30964  grpoinveu  31001  5oalem4  32139  rnbra  32589  xreceu  33368  bnj594  35422  bnj953  35449  scottsn  35634  fnsingle  36497  funimage  36506  funtransport  36612  funray  36721  funline  36723  hilbert1.2  36736  lineintmo  36738  bj-bary1  38065  poimirlem13  38383  poimirlem14  38384  poimirlem17  38387  poimirlem27  38397  mopre  39220  sucmapleftuniq  39239  antisymressn  39283  disjdmqscossss  39655  prter2  39755  cdleme  41434  rediveud  43319  kelac2lem  43906  frege124d  44602  2ffzoeq  48217  sprsymrelf1lem  48392  paireqne  48412  usgrexmpl2trifr  48954  gpg5grlic  49011  pgnbgreunbgrlem2  49034  mof0ALT  49769  mofsn  49773  f1omoOLD  49821  oppcendc  49945