Theorem eqtr3 2843

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

Syntax hints:   → wi 4   ∧ wa 398   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2124  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-cleq 2814

This theorem is referenced by:  neneor  3118  moeq  3698  euind  3715  reuind  3744  disjeq0  4405  ssprsseq  4758  mosneq  4773  prnebg  4786  prnesn  4790  prel12g  4794  3elpr2eq  4837  eusv1  5292  xpcan  6033  xpcan2  6034  funopg  6389  foco  6602  funopdmsn  6912  funsndifnop  6913  mpofun  7276  wfr3g  7953  oawordeulem  8180  ixpfi2  8822  isf32lem2  9776  fpwwe2lem13  10064  1re  10641  receu  11285  xrlttri  12533  injresinjlem  13158  cshwsexa  14186  fsumparts  15161  odd2np1  15690  prmreclem2  16253  divsfval  16820  isprs  17540  psrn  17819  grpinveu  18138  symgextf1  18549  symgfixf1  18565  efgrelexlemb  18876  lspextmo  19828  evlseu  20296  tgcmp  22009  sqf11  25716  dchrisumlem2  26066  axlowdimlem15  26742  axcontlem2  26751  wlksoneq1eq2  27446  spthonepeq  27533  uspgrn2crct  27586  wwlksnextinj  27677  frgrwopreglem5lem  28099  numclwwlk1lem2f1  28136  nsnlplig  28258  nsnlpligALT  28259  grpoinveu  28296  5oalem4  29434  rnbra  29884  xreceu  30598  bnj594  32184  bnj953  32211  frr3g  33121  sltsolem1  33180  nocvxminlem  33247  fnsingle  33380  funimage  33389  funtransport  33492  funray  33601  funline  33603  hilbert1.2  33616  lineintmo  33618  bj-bary1  34596  poimirlem13  34920  poimirlem14  34921  poimirlem17  34924  poimirlem27  34934  prter2  36032  cdleme  37711  kelac2lem  39684  frege124d  40126  2ffzoeq  43548  sprsymrelf1lem  43673  paireqne  43693