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 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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  neneor  3061  moeq  3668  euind  3685  reuind  3714  disjeq0  4412  ssprsseq  4786  mosneq  4802  prnebg  4816  prnesn  4820  prel12g  4824  3elpr2eq  4839  eusv1  5360  axprglem  5401  xpcan  6186  xpcan2  6187  funopg  6602  funopdmsn  7186  funsndifnop  7187  fvf1pr  7346  resf1extb  7980  wfr3g  8375  oawordeulem  8600  nnasmo  8710  en1eqsn  9304  ixpfi2  9377  frr3g  9797  isf32lem2  10471  fpwwe2lem12  10766  1re  11347  receu  12001  xrlttri  13308  injresinjlem  13965  fsumparts  16017  odd2np1  16555  prmreclem2  17139  divsfval  17769  isprs  18520  psrn  18799  grpinveu  19235  symgextf1  19686  symgfixf1  19702  efgrelexlemb  20015  lspextmo  21382  evlseu  22447  tgcmp  23774  sqf11  27523  dchrisumlem2  27874  ltssolem1  28089  nocvxminlem  28197  divsmo  28627  axlowdimlem15  29591  axcontlem2  29600  wlksoneq1eq2  30300  spthonepeq  30395  uspgrn2crct  30454  wwlksnextinj  30545  frgrwopreglem5lem  30978  numclwwlk1lem2f1  31015  nsnlplig  31140  nsnlpligALT  31141  grpoinveu  31178  5oalem4  32316  rnbra  32766  xreceu  33584  bnj594  35653  bnj953  35680  ordunmax  35833  scottsn  35875  fnsingle  36896  funimage  36905  funtransport  37011  funray  37120  funline  37122  hilbert1.2  37135  lineintmo  37137  bj-bary1  38501  poimirlem13  38819  poimirlem14  38820  poimirlem17  38823  poimirlem27  38833  mopre  39669  sucmapleftuniq  39688  antisymressn  39732  disjdmqscossss  40104  prter2  40204  cdleme  41883  rediveud  43760  kelac2lem  44332  frege124d  45022  2ffzoeq  48671  sprsymrelf1lem  48846  paireqne  48866  usgrexmpl2trifr  49408  gpg5grlic  49465  pgnbgreunbgrlem2  49488  mof0ALT  50282  mofsn  50286  f1omoOLD  50339  oppcendc  50463  parhomidval  51077