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 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

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

This theorem is referenced by:  neneor  3118  moeq  3698  euind  3715  reuind  3744  disjeq0  4405  ssprsseq  4752  mosneq  4767  prnebg  4780  prnesn  4784  prel12g  4788  3elpr2eq  4831  eusv1  5284  xpcan  6028  xpcan2  6029  funopg  6384  foco  6597  funopdmsn  6907  funsndifnop  6908  mpofun  7270  wfr3g  7947  oawordeulem  8174  ixpfi2  8816  isf32lem2  9770  fpwwe2lem13  10058  1re  10635  receu  11279  xrlttri  12526  injresinjlem  13151  cshwsexa  14180  fsumparts  15155  odd2np1  15684  prmreclem2  16247  divsfval  16814  isprs  17534  psrn  17813  grpinveu  18132  symgextf1  18543  symgfixf1  18559  efgrelexlemb  18870  lspextmo  19822  evlseu  20290  tgcmp  22003  sqf11  25710  dchrisumlem2  26060  axlowdimlem15  26736  axcontlem2  26745  wlksoneq1eq2  27440  spthonepeq  27527  uspgrn2crct  27580  wwlksnextinj  27671  frgrwopreglem5lem  28093  numclwwlk1lem2f1  28130  nsnlplig  28252  nsnlpligALT  28253  grpoinveu  28290  5oalem4  29428  rnbra  29878  xreceu  30593  bnj594  32179  bnj953  32206  frr3g  33116  sltsolem1  33175  nocvxminlem  33242  fnsingle  33375  funimage  33384  funtransport  33487  funray  33596  funline  33598  hilbert1.2  33611  lineintmo  33613  bj-bary1  34587  poimirlem13  34899  poimirlem14  34900  poimirlem17  34903  poimirlem27  34913  prter2  36011  cdleme  37690  kelac2lem  39657  frege124d  40099  2ffzoeq  43521  sprsymrelf1lem  43646  paireqne  43666