Theorem eqtr3 2765

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  neneor  3045  moeq  3643  euind  3660  reuind  3689  disjeq0  4390  ssprsseq  4759  mosneq  4774  prnebg  4787  prnesn  4791  prel12g  4795  3elpr2eq  4839  eusv1  5315  xpcan  6084  xpcan2  6085  funopg  6475  funopdmsn  7031  funsndifnop  7032  mpofunOLD  7408  wfr3g  8147  oawordeulem  8394  nnasmo  8502  ixpfi2  9126  frr3g  9523  isf32lem2  10119  fpwwe2lem12  10407  1re  10984  receu  11629  xrlttri  12882  injresinjlem  13516  cshwsexa  14546  fsumparts  15527  odd2np1  16059  prmreclem2  16627  divsfval  17267  isprs  18024  psrn  18302  grpinveu  18623  symgextf1  19038  symgfixf1  19054  efgrelexlemb  19365  lspextmo  20327  evlseu  21302  tgcmp  22561  sqf11  26297  dchrisumlem2  26647  axlowdimlem15  27333  axcontlem2  27342  wlksoneq1eq2  28041  spthonepeq  28129  uspgrn2crct  28182  wwlksnextinj  28273  frgrwopreglem5lem  28693  numclwwlk1lem2f1  28730  nsnlplig  28852  nsnlpligALT  28853  grpoinveu  28890  5oalem4  30028  rnbra  30478  xreceu  31205  bnj594  32901  bnj953  32928  sltsolem1  33887  nocvxminlem  33981  fnsingle  34230  funimage  34239  funtransport  34342  funray  34451  funline  34453  hilbert1.2  34466  lineintmo  34468  bj-bary1  35492  poimirlem13  35799  poimirlem14  35800  poimirlem17  35803  poimirlem27  35813  prter2  36902  cdleme  38581  kelac2lem  40896  frege124d  41376  2ffzoeq  44831  sprsymrelf1lem  44954  paireqne  44974  mof0ALT  46178  mofsn  46182  f1omo  46199