Theorem eqtr3 2631

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 2617	. 2 ⊢ (𝐵 = 𝐶 ↔ 𝐶 = 𝐵)
2		eqtr 2629	. 2 ⊢ ((𝐴 = 𝐶 ∧ 𝐶 = 𝐵) → 𝐴 = 𝐵)
3	1, 2	sylan2b 491	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-cleq 2603

This theorem is referenced by:  neneor  2881  eueq  3345  euind  3360  reuind  3378  ssprsseq  4297  prnebg  4329  preqsnOLD  4332  eusv1  4786  restidsingOLD  5378  xpcan  5489  xpcan2  5490  funopg  5836  foco  6038  funsndifnop  6321  mpt2fun  6660  wfr3g  7300  oawordeulem  7521  ixpfi2  8147  wemapso2lem  8340  isf32lem2  9059  fpwwe2lem13  9343  1re  9918  receu  10551  xrlttri  11848  injresinjlem  12450  cshwsexa  13421  fsumparts  14379  odd2np1  14903  prmreclem2  15459  divsfval  16030  isprs  16753  psrn  17032  grpinveu  17279  symgextf1  17664  symgfixf1  17680  efgrelexlemb  17986  lspextmo  18877  evlseu  19337  tgcmp  21014  sqf11  24665  dchrisumlem2  24979  axlowdimlem15  25636  axcontlem2  25645  nbgraf1olem1  25970  spthonepeq  26117  usgrcyclnl2  26169  4cycl4dv  26195  wwlkextinj  26258  numclwlk1lem2f1  26621  grpoinveu  26757  5oalem4  27900  rnbra  28350  xreceu  28961  bnj594  30236  bnj953  30263  frr3g  31023  sltsolem1  31067  nocvxminlem  31089  fnsingle  31196  funimage  31205  funtransport  31308  funray  31417  funline  31419  hilbert1.2  31432  lineintmo  31434  bj-bary1  32339  poimirlem13  32592  poimirlem14  32593  poimirlem17  32596  poimirlem27  32606  prtlem11  33169  prter2  33184  cdleme  34866  kelac2lem  36652  frege124d  37072  2ffzoeq  40361  wlksoneq1eq2  40872  spthonepeq-av  40958  uspgrn2crct  41011  wwlksnextinj  41105  av-numclwlk1lem2f1  41524