Theorem eqtr3 2753

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 2743	. 2 ⊢ (𝐵 = 𝐶 → (𝐴 = 𝐵 ↔ 𝐴 = 𝐶))
2	1	biimparc 479	1 ⊢ ((𝐴 = 𝐶 ∧ 𝐵 = 𝐶) → 𝐴 = 𝐵)

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

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 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  neneor  3028  moeq  3661  euind  3678  reuind  3707  disjeq0  4401  ssprsseq  4772  mosneq  4789  prnebg  4803  prnesn  4807  prel12g  4811  3elpr2eq  4853  eusv1  5324  xpcan  6118  xpcan2  6119  funopg  6510  funopdmsn  7078  funsndifnop  7079  fvf1pr  7236  resf1extb  7859  wfr3g  8244  oawordeulem  8464  nnasmo  8573  en1eqsn  9154  ixpfi2  9229  frr3g  9644  isf32lem2  10240  fpwwe2lem12  10528  1re  11107  receu  11757  xrlttri  13033  injresinjlem  13685  fsumparts  15708  odd2np1  16247  prmreclem2  16824  divsfval  17446  isprs  18197  psrn  18476  grpinveu  18882  symgextf1  19328  symgfixf1  19344  efgrelexlemb  19657  lspextmo  20985  evlseu  22013  tgcmp  23311  sqf11  27071  dchrisumlem2  27423  sltsolem1  27609  nocvxminlem  27712  divsmo  28118  axlowdimlem15  28929  axcontlem2  28938  wlksoneq1eq2  29636  spthonepeq  29725  uspgrn2crct  29781  wwlksnextinj  29872  frgrwopreglem5lem  30292  numclwwlk1lem2f1  30329  nsnlplig  30453  nsnlpligALT  30454  grpoinveu  30491  5oalem4  31629  rnbra  32079  xreceu  32894  bnj594  34916  bnj953  34943  fnsingle  35953  funimage  35962  funtransport  36065  funray  36174  funline  36176  hilbert1.2  36189  lineintmo  36191  bj-bary1  37346  poimirlem13  37673  poimirlem14  37674  poimirlem17  37677  poimirlem27  37687  antisymressn  38481  disjdmqscossss  38841  prter2  38920  cdleme  40599  rediveud  42476  kelac2lem  43097  frege124d  43794  2ffzoeq  47358  sprsymrelf1lem  47522  paireqne  47542  usgrexmpl2trifr  48068  gpg5grlic  48125  pgnbgreunbgrlem2  48148  mof0ALT  48871  mofsn  48875  f1omoOLD  48925  oppcendc  49050