Theorem eqtr3 2785

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755

This theorem is referenced by:  neneor  3060  moeq  3670  euind  3687  reuind  3716  disjeq0  4416  ssprsseq  4791  mosneq  4807  prnebg  4821  prnesn  4825  prel12g  4829  3elpr2eq  4871  eusv1  5362  axprglem  5407  xpcan  6174  xpcan2  6175  funopg  6570  funopdmsn  7147  funsndifnop  7148  fvf1pr  7305  resf1extb  7927  wfr3g  8312  oawordeulem  8535  nnasmo  8645  en1eqsn  9231  ixpfi2  9303  frr3g  9724  isf32lem2  10333  fpwwe2lem12  10622  1re  11203  receu  11854  xrlttri  13159  injresinjlem  13815  fsumparts  15854  odd2np1  16394  prmreclem2  16972  divsfval  17596  isprs  18347  psrn  18626  grpinveu  19036  symgextf1  19486  symgfixf1  19502  efgrelexlemb  19815  lspextmo  21177  evlseu  22234  tgcmp  23558  sqf11  27303  dchrisumlem2  27654  ltssolem1  27839  nocvxminlem  27947  divsmo  28377  axlowdimlem15  29306  axcontlem2  29315  wlksoneq1eq2  30012  spthonepeq  30101  uspgrn2crct  30157  wwlksnextinj  30248  frgrwopreglem5lem  30671  numclwwlk1lem2f1  30708  nsnlplig  30833  nsnlpligALT  30834  grpoinveu  30871  5oalem4  32009  rnbra  32459  xreceu  33241  bnj594  35300  bnj953  35327  scottsn  35520  fnsingle  36409  funimage  36418  funtransport  36523  funray  36632  funline  36634  hilbert1.2  36647  lineintmo  36649  bj-bary1  37956  poimirlem13  38284  poimirlem14  38285  poimirlem17  38288  poimirlem27  38298  mopre  39120  sucmapleftuniq  39139  antisymressn  39183  disjdmqscossss  39555  prter2  39655  cdleme  41334  rediveud  43204  kelac2lem  43791  frege124d  44487  2ffzoeq  48065  sprsymrelf1lem  48240  paireqne  48260  usgrexmpl2trifr  48802  gpg5grlic  48859  pgnbgreunbgrlem2  48882  mof0ALT  49618  mofsn  49622  f1omoOLD  49672  oppcendc  49796