Theorem eqtr3 2820

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  neneor  3086  moeq  3646  euind  3663  reuind  3692  disjeq0  4363  ssprsseq  4718  mosneq  4733  prnebg  4746  prnesn  4750  prel12g  4754  3elpr2eq  4799  eusv1  5257  xpcan  6000  xpcan2  6001  funopg  6358  foco  6577  funopdmsn  6889  funsndifnop  6890  mpofun  7255  wfr3g  7936  oawordeulem  8163  ixpfi2  8806  isf32lem2  9765  fpwwe2lem13  10053  1re  10630  receu  11274  xrlttri  12520  injresinjlem  13152  cshwsexa  14177  fsumparts  15153  odd2np1  15682  prmreclem2  16243  divsfval  16812  isprs  17532  psrn  17811  grpinveu  18130  symgextf1  18541  symgfixf1  18557  efgrelexlemb  18868  lspextmo  19821  evlseu  20755  tgcmp  22006  sqf11  25724  dchrisumlem2  26074  axlowdimlem15  26750  axcontlem2  26759  wlksoneq1eq2  27454  spthonepeq  27541  uspgrn2crct  27594  wwlksnextinj  27685  frgrwopreglem5lem  28105  numclwwlk1lem2f1  28142  nsnlplig  28264  nsnlpligALT  28265  grpoinveu  28302  5oalem4  29440  rnbra  29890  xreceu  30624  bnj594  32294  bnj953  32321  frr3g  33234  sltsolem1  33293  nocvxminlem  33360  fnsingle  33493  funimage  33502  funtransport  33605  funray  33714  funline  33716  hilbert1.2  33729  lineintmo  33731  bj-bary1  34726  poimirlem13  35070  poimirlem14  35071  poimirlem17  35074  poimirlem27  35084  prter2  36177  cdleme  37856  kelac2lem  40008  frege124d  40462  2ffzoeq  43885  sprsymrelf1lem  44008  paireqne  44028