Theorem eqtr3 2760

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  neneor  3039  moeq  3715  euind  3732  reuind  3761  disjeq0  4461  ssprsseq  4829  mosneq  4846  prnebg  4860  prnesn  4864  prel12g  4868  3elpr2eq  4910  eusv1  5396  xpcan  6197  xpcan2  6198  funopg  6601  funopdmsn  7169  funsndifnop  7170  fvf1pr  7326  wfr3g  8345  oawordeulem  8590  nnasmo  8699  en1eqsn  9305  ixpfi2  9387  frr3g  9793  isf32lem2  10391  fpwwe2lem12  10679  1re  11258  receu  11905  xrlttri  13177  injresinjlem  13822  cshwsexaOLD  14859  fsumparts  15838  odd2np1  16374  prmreclem2  16950  divsfval  17593  isprs  18353  psrn  18632  grpinveu  19004  symgextf1  19453  symgfixf1  19469  efgrelexlemb  19782  lspextmo  21072  evlseu  22124  tgcmp  23424  sqf11  27196  dchrisumlem2  27548  sltsolem1  27734  nocvxminlem  27836  divsmo  28224  axlowdimlem15  28985  axcontlem2  28994  wlksoneq1eq2  29696  spthonepeq  29784  uspgrn2crct  29837  wwlksnextinj  29928  frgrwopreglem5lem  30348  numclwwlk1lem2f1  30385  nsnlplig  30509  nsnlpligALT  30510  grpoinveu  30547  5oalem4  31685  rnbra  32135  xreceu  32888  bnj594  34904  bnj953  34931  fnsingle  35900  funimage  35909  funtransport  36012  funray  36121  funline  36123  hilbert1.2  36136  lineintmo  36138  bj-bary1  37294  poimirlem13  37619  poimirlem14  37620  poimirlem17  37623  poimirlem27  37633  antisymressn  38425  disjdmqscossss  38784  prter2  38862  cdleme  40542  kelac2lem  43052  frege124d  43750  2ffzoeq  47276  sprsymrelf1lem  47415  paireqne  47435  usgrexmpl2trifr  47931  gpg5grlic  47974  mof0ALT  48669  mofsn  48673  f1omo  48690