Theorem eqtr3 2630

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

Syntax hints:   → wi 4   ∧ wa 382   = wceq 1474

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-an 384  df-cleq 2602

This theorem is referenced by:  neneor  2880  eueq  3344  euind  3359  reuind  3377  prnebg  4324  preqsnOLD  4327  eusv1  4781  restidsingOLD  5365  xpcan  5475  xpcan2  5476  funopg  5822  foco  6023  mpt2fun  6638  wfr3g  7277  oawordeulem  7498  ixpfi2  8124  wemapso2lem  8317  isf32lem2  9036  fpwwe2lem13  9320  1re  9895  receu  10521  xrlttri  11807  injresinjlem  12405  cshwsexa  13367  fsumparts  14325  odd2np1  14849  prmreclem2  15405  divsfval  15976  isprs  16699  psrn  16978  grpinveu  17225  symgextf1  17610  symgfixf1  17626  efgrelexlemb  17932  lspextmo  18823  evlseu  19283  tgcmp  20956  sqf11  24582  dchrisumlem2  24896  axlowdimlem15  25554  axcontlem2  25563  nbgraf1olem1  25736  spthonepeq  25883  usgrcyclnl2  25935  4cycl4dv  25961  wwlkextinj  26024  numclwlk1lem2f1  26387  grpoinveu  26523  5oalem4  27706  rnbra  28156  xreceu  28767  bnj594  30042  bnj953  30069  frr3g  30829  sltsolem1  30873  nocvxminlem  30895  fnsingle  31002  funimage  31011  funtransport  31114  funray  31223  funline  31225  hilbert1.2  31238  lineintmo  31240  bj-bary1  32135  poimirlem13  32388  poimirlem14  32389  poimirlem17  32392  poimirlem27  32402  prtlem11  32965  prter2  32980  cdleme  34662  kelac2lem  36448  frege124d  36868  ssprsseq  40122  funsndifnop  40141  2ffzoeq  40181  wlksoneq1eq2  40867  spthonepeq-av  40953  uspgrn2crct  41006  wwlksnextinj  41100  av-numclwlk1lem2f1  41519