Theorem eqtr3 2784

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 2774	. 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 2734

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

This theorem is used by:  neneor  3059  moeq  3668  euind  3685  reuind  3714  disjeq0  4412  ssprsseq  4789  mosneq  4805  prnebg  4819  prnesn  4823  prel12g  4827  3elpr2eq  4869  eusv1  5360  axprglem  5405  xpcan  6173  xpcan2  6174  funopg  6571  funopdmsn  7151  funsndifnop  7152  fvf1pr  7312  resf1extb  7935  wfr3g  8322  oawordeulem  8545  nnasmo  8655  en1eqsn  9249  ixpfi2  9321  frr3g  9742  isf32lem2  10360  fpwwe2lem12  10655  1re  11236  receu  11887  xrlttri  13194  injresinjlem  13850  fsumparts  15897  odd2np1  16437  prmreclem2  17015  divsfval  17639  isprs  18390  psrn  18669  grpinveu  19104  symgextf1  19554  symgfixf1  19570  efgrelexlemb  19883  lspextmo  21246  evlseu  22305  tgcmp  23632  sqf11  27383  dchrisumlem2  27734  ltssolem1  27919  nocvxminlem  28027  divsmo  28457  axlowdimlem15  29421  axcontlem2  29430  wlksoneq1eq2  30130  spthonepeq  30225  uspgrn2crct  30284  wwlksnextinj  30375  frgrwopreglem5lem  30808  numclwwlk1lem2f1  30845  nsnlplig  30970  nsnlpligALT  30971  grpoinveu  31008  5oalem4  32146  rnbra  32596  xreceu  33375  bnj594  35429  bnj953  35456  scottsn  35641  fnsingle  36504  funimage  36513  funtransport  36619  funray  36728  funline  36730  hilbert1.2  36743  lineintmo  36745  bj-bary1  38072  poimirlem13  38390  poimirlem14  38391  poimirlem17  38394  poimirlem27  38404  mopre  39227  sucmapleftuniq  39246  antisymressn  39290  disjdmqscossss  39662  prter2  39762  cdleme  41441  rediveud  43326  kelac2lem  43913  frege124d  44609  2ffzoeq  48224  sprsymrelf1lem  48399  paireqne  48419  usgrexmpl2trifr  48961  gpg5grlic  49018  pgnbgreunbgrlem2  49041  mof0ALT  49776  mofsn  49780  f1omoOLD  49828  oppcendc  49952