Theorem eqtr3 2783

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 2773	. 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 2733

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

This theorem is used by:  neneor  3058  moeq  3665  euind  3682  reuind  3711  disjeq0  4409  ssprsseq  4786  mosneq  4802  prnebg  4816  prnesn  4820  prel12g  4824  3elpr2eq  4866  eusv1  5353  axprglem  5394  xpcan  6168  xpcan2  6169  funopg  6574  funopdmsn  7154  funsndifnop  7155  fvf1pr  7315  resf1extb  7946  wfr3g  8337  oawordeulem  8562  nnasmo  8672  en1eqsn  9266  ixpfi2  9339  frr3g  9760  isf32lem2  10432  fpwwe2lem12  10727  1re  11308  receu  11961  xrlttri  13268  injresinjlem  13925  fsumparts  15973  odd2np1  16511  prmreclem2  17095  divsfval  17719  isprs  18470  psrn  18749  grpinveu  19185  symgextf1  19635  symgfixf1  19651  efgrelexlemb  19964  lspextmo  21331  evlseu  22392  tgcmp  23719  sqf11  27466  dchrisumlem2  27817  ltssolem1  28032  nocvxminlem  28140  divsmo  28570  axlowdimlem15  29534  axcontlem2  29543  wlksoneq1eq2  30243  spthonepeq  30338  uspgrn2crct  30397  wwlksnextinj  30488  frgrwopreglem5lem  30921  numclwwlk1lem2f1  30958  nsnlplig  31083  nsnlpligALT  31084  grpoinveu  31121  5oalem4  32259  rnbra  32709  xreceu  33488  bnj594  35542  bnj953  35569  scottsn  35750  fnsingle  36681  funimage  36690  funtransport  36796  funray  36905  funline  36907  hilbert1.2  36920  lineintmo  36922  bj-bary1  38233  poimirlem13  38551  poimirlem14  38552  poimirlem17  38555  poimirlem27  38565  mopre  39403  sucmapleftuniq  39422  antisymressn  39466  disjdmqscossss  39838  prter2  39938  cdleme  41617  rediveud  43494  kelac2lem  44065  frege124d  44760  2ffzoeq  48397  sprsymrelf1lem  48572  paireqne  48592  usgrexmpl2trifr  49134  gpg5grlic  49191  pgnbgreunbgrlem2  49214  mof0ALT  49949  mofsn  49953  f1omoOLD  50001  oppcendc  50125