Theorem eqtr3 2757

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  neneor  3041  moeq  3668  euind  3685  reuind  3714  disjeq0  4420  ssprsseq  4790  mosneq  4805  prnebg  4818  prnesn  4822  prel12g  4826  3elpr2eq  4869  eusv1  5351  xpcan  6133  xpcan2  6134  funopg  6540  funopdmsn  7101  funsndifnop  7102  mpofunOLD  7486  wfr3g  8258  oawordeulem  8506  nnasmo  8614  en1eqsn  9225  ixpfi2  9301  frr3g  9701  isf32lem2  10299  fpwwe2lem12  10587  1re  11164  receu  11809  xrlttri  13068  injresinjlem  13702  cshwsexaOLD  14725  fsumparts  15702  odd2np1  16234  prmreclem2  16800  divsfval  17443  isprs  18200  psrn  18478  grpinveu  18799  symgextf1  19217  symgfixf1  19233  efgrelexlemb  19546  lspextmo  20574  evlseu  21530  tgcmp  22789  sqf11  26525  dchrisumlem2  26875  sltsolem1  27060  nocvxminlem  27160  axlowdimlem15  27968  axcontlem2  27977  wlksoneq1eq2  28675  spthonepeq  28763  uspgrn2crct  28816  wwlksnextinj  28907  frgrwopreglem5lem  29327  numclwwlk1lem2f1  29364  nsnlplig  29486  nsnlpligALT  29487  grpoinveu  29524  5oalem4  30662  rnbra  31112  xreceu  31848  bnj594  33613  bnj953  33640  fnsingle  34580  funimage  34589  funtransport  34692  funray  34801  funline  34803  hilbert1.2  34816  lineintmo  34818  bj-bary1  35856  poimirlem13  36164  poimirlem14  36165  poimirlem17  36168  poimirlem27  36178  antisymressn  36979  disjdmqscossss  37338  prter2  37416  cdleme  39096  kelac2lem  41449  frege124d  42155  2ffzoeq  45680  sprsymrelf1lem  45803  paireqne  45823  mof0ALT  47026  mofsn  47030  f1omo  47047