Theorem eqtr3 2755

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725

This theorem is referenced by:  neneor  3030  moeq  3663  euind  3680  reuind  3709  disjeq0  4407  ssprsseq  4778  mosneq  4795  prnebg  4809  prnesn  4813  prel12g  4817  3elpr2eq  4859  eusv1  5333  xpcan  6131  xpcan2  6132  funopg  6523  funopdmsn  7092  funsndifnop  7093  fvf1pr  7250  resf1extb  7873  wfr3g  8258  oawordeulem  8478  nnasmo  8587  en1eqsn  9169  ixpfi2  9244  frr3g  9659  isf32lem2  10255  fpwwe2lem12  10543  1re  11122  receu  11772  xrlttri  13048  injresinjlem  13700  fsumparts  15723  odd2np1  16262  prmreclem2  16839  divsfval  17461  isprs  18212  psrn  18491  grpinveu  18897  symgextf1  19343  symgfixf1  19359  efgrelexlemb  19672  lspextmo  21000  evlseu  22028  tgcmp  23326  sqf11  27086  dchrisumlem2  27438  sltsolem1  27624  nocvxminlem  27727  divsmo  28133  axlowdimlem15  28945  axcontlem2  28954  wlksoneq1eq2  29652  spthonepeq  29741  uspgrn2crct  29797  wwlksnextinj  29888  frgrwopreglem5lem  30311  numclwwlk1lem2f1  30348  nsnlplig  30472  nsnlpligALT  30473  grpoinveu  30510  5oalem4  31648  rnbra  32098  xreceu  32913  bnj594  34935  bnj953  34962  fnsingle  35972  funimage  35981  funtransport  36086  funray  36195  funline  36197  hilbert1.2  36210  lineintmo  36212  bj-bary1  37367  poimirlem13  37683  poimirlem14  37684  poimirlem17  37687  poimirlem27  37697  mopre  38494  sucmapleftuniq  38512  antisymressn  38556  disjdmqscossss  38911  prter2  38990  cdleme  40669  rediveud  42551  kelac2lem  43171  frege124d  43868  2ffzoeq  47441  sprsymrelf1lem  47605  paireqne  47625  usgrexmpl2trifr  48151  gpg5grlic  48208  pgnbgreunbgrlem2  48231  mof0ALT  48954  mofsn  48958  f1omoOLD  49008  oppcendc  49133