Theorem eqtr3 2781

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2753

This theorem is referenced by:  neneor  3031  eueq  3519  euind  3534  reuind  3552  disjeq0  4166  ssprsseq  4502  prnebg  4533  prnesn  4538  preqsnOLDOLD  4542  prel12g  4544  3elpr2eq  4587  eusv1  5009  restidsingOLD  5617  xpcan  5728  xpcan2  5729  funopg  6083  foco  6287  funopdmsn  6579  funsndifnop  6580  mpt2fun  6928  wfr3g  7583  oawordeulem  7805  ixpfi2  8431  wemapso2lem  8624  isf32lem2  9388  fpwwe2lem13  9676  1re  10251  receu  10884  xrlttri  12185  injresinjlem  12802  cshwsexa  13790  fsumparts  14757  odd2np1  15287  prmreclem2  15843  divsfval  16429  isprs  17151  psrn  17430  grpinveu  17677  symgextf1  18061  symgfixf1  18077  efgrelexlemb  18383  lspextmo  19278  evlseu  19738  tgcmp  21426  sqf11  25085  dchrisumlem2  25399  axlowdimlem15  26056  axcontlem2  26065  wlksoneq1eq2  26791  spthonepeq  26879  uspgrn2crct  26932  wwlksnextinj  27038  frgrwopreglem5lem  27495  numclwlk1lem2f1  27537  nsnlplig  27665  nsnlpligALT  27666  grpoinveu  27703  5oalem4  28846  rnbra  29296  xreceu  29960  bnj594  31310  bnj953  31337  frr3g  32106  sltsolem1  32153  nocvxminlem  32220  fnsingle  32353  funimage  32362  funtransport  32465  funray  32574  funline  32576  hilbert1.2  32589  lineintmo  32591  bj-bary1  33491  poimirlem13  33753  poimirlem14  33754  poimirlem17  33757  poimirlem27  33767  prtlem11  34673  prter2  34688  cdleme  36368  kelac2lem  38154  frege124d  38573  2ffzoeq  41866  sprsymrelf1lem  42269