Theorem eqtr3 2752

Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.) (Proof shortened by Wolf Lammen, 24-Oct-2024.)

Assertion

Ref	Expression
eqtr3	⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

Proof of Theorem eqtr3

Step	Hyp	Ref	Expression
1		eqeq2 2742	. 2 ⊢ (𝐵 = 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
2	1	biimparc 479	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722

This theorem is referenced by:  neneor  3026  moeq  3681  euind  3698  reuind  3727  disjeq0  4422  ssprsseq  4792  mosneq  4809  prnebg  4823  prnesn  4827  prel12g  4831  3elpr2eq  4873  eusv1  5349  xpcan  6152  xpcan2  6153  funopg  6553  funopdmsn  7125  funsndifnop  7126  fvf1pr  7285  resf1extb  7913  wfr3g  8301  oawordeulem  8521  nnasmo  8630  en1eqsn  9226  ixpfi2  9308  frr3g  9716  isf32lem2  10314  fpwwe2lem12  10602  1re  11181  receu  11830  xrlttri  13106  injresinjlem  13755  cshwsexaOLD  14797  fsumparts  15779  odd2np1  16318  prmreclem2  16895  divsfval  17517  isprs  18264  psrn  18541  grpinveu  18913  symgextf1  19358  symgfixf1  19374  efgrelexlemb  19687  lspextmo  20970  evlseu  21997  tgcmp  23295  sqf11  27056  dchrisumlem2  27408  sltsolem1  27594  nocvxminlem  27696  divsmo  28094  axlowdimlem15  28890  axcontlem2  28899  wlksoneq1eq2  29599  spthonepeq  29689  uspgrn2crct  29745  wwlksnextinj  29836  frgrwopreglem5lem  30256  numclwwlk1lem2f1  30293  nsnlplig  30417  nsnlpligALT  30418  grpoinveu  30455  5oalem4  31593  rnbra  32043  xreceu  32849  bnj594  34909  bnj953  34936  fnsingle  35914  funimage  35923  funtransport  36026  funray  36135  funline  36137  hilbert1.2  36150  lineintmo  36152  bj-bary1  37307  poimirlem13  37634  poimirlem14  37635  poimirlem17  37638  poimirlem27  37648  antisymressn  38442  disjdmqscossss  38802  prter2  38881  cdleme  40561  rediveud  42438  kelac2lem  43060  frege124d  43757  2ffzoeq  47332  sprsymrelf1lem  47496  paireqne  47516  usgrexmpl2trifr  48032  gpg5grlic  48088  pgnbgreunbgrlem2  48111  mof0ALT  48832  mofsn  48836  f1omoOLD  48886  oppcendc  49011