Theorem eqtr3 2672

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.)

Assertion

Ref	Expression
eqtr3	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

Proof of Theorem eqtr3

Step	Hyp	Ref	Expression
1		eqcom 2658	. 2 ⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵)
2		eqtr 2670	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐵) → 𝐴 = 𝐵)
3	1, 2	sylan2b 491	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1523

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644

This theorem is referenced by:  neneor  2922  eueq  3411  euind  3426  reuind  3444  ssprsseq  4389  prnebg  4420  preqsnOLD  4425  3elpr2eq  4467  eusv1  4890  restidsingOLD  5494  xpcan  5605  xpcan2  5606  funopg  5960  foco  6163  funopdmsn  6455  funsndifnop  6456  mpt2fun  6804  wfr3g  7458  oawordeulem  7679  ixpfi2  8305  wemapso2lem  8498  isf32lem2  9214  fpwwe2lem13  9502  1re  10077  receu  10710  xrlttri  12010  injresinjlem  12628  cshwsexa  13616  fsumparts  14582  odd2np1  15112  prmreclem2  15668  divsfval  16254  isprs  16977  psrn  17256  grpinveu  17503  symgextf1  17887  symgfixf1  17903  efgrelexlemb  18209  lspextmo  19104  evlseu  19564  tgcmp  21252  sqf11  24910  dchrisumlem2  25224  axlowdimlem15  25881  axcontlem2  25890  wlksoneq1eq2  26616  spthonepeq  26704  uspgrn2crct  26756  wwlksnextinj  26862  frgrwopreglem5lem  27300  numclwlk1lem2f1  27347  nsnlplig  27463  nsnlpligALT  27464  grpoinveu  27501  5oalem4  28644  rnbra  29094  xreceu  29758  bnj594  31108  bnj953  31135  frr3g  31904  sltsolem1  31951  nocvxminlem  32018  fnsingle  32151  funimage  32160  funtransport  32263  funray  32372  funline  32374  hilbert1.2  32387  lineintmo  32389  bj-bary1  33292  poimirlem13  33552  poimirlem14  33553  poimirlem17  33556  poimirlem27  33566  prtlem11  34470  prter2  34485  cdleme  36165  kelac2lem  37951  frege124d  38370  2ffzoeq  41663  sprsymrelf1lem  42066