Theorem eqtr3 2756

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 2746	. 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 2123  ax-ext 2706

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

This theorem is referenced by:  neneor  3030  moeq  3663  euind  3680  reuind  3709  disjeq0  4406  ssprsseq  4779  mosneq  4796  prnebg  4810  prnesn  4814  prel12g  4818  3elpr2eq  4860  eusv1  5334  xpcan  6132  xpcan2  6133  funopg  6524  funopdmsn  7093  funsndifnop  7094  fvf1pr  7251  resf1extb  7874  wfr3g  8259  oawordeulem  8479  nnasmo  8589  en1eqsn  9173  ixpfi2  9248  frr3g  9666  isf32lem2  10262  fpwwe2lem12  10551  1re  11130  receu  11780  xrlttri  13051  injresinjlem  13704  fsumparts  15727  odd2np1  16266  prmreclem2  16843  divsfval  17466  isprs  18217  psrn  18496  grpinveu  18902  symgextf1  19348  symgfixf1  19364  efgrelexlemb  19677  lspextmo  21006  evlseu  22036  tgcmp  23343  sqf11  27103  dchrisumlem2  27455  sltsolem1  27641  nocvxminlem  27744  divsmo  28153  axlowdimlem15  28978  axcontlem2  28987  wlksoneq1eq2  29685  spthonepeq  29774  uspgrn2crct  29830  wwlksnextinj  29921  frgrwopreglem5lem  30344  numclwwlk1lem2f1  30381  nsnlplig  30505  nsnlpligALT  30506  grpoinveu  30543  5oalem4  31681  rnbra  32131  xreceu  32952  bnj594  35017  bnj953  35044  fnsingle  36060  funimage  36069  funtransport  36174  funray  36283  funline  36285  hilbert1.2  36298  lineintmo  36300  bj-bary1  37456  poimirlem13  37773  poimirlem14  37774  poimirlem17  37777  poimirlem27  37787  mopre  38584  sucmapleftuniq  38602  antisymressn  38646  disjdmqscossss  39001  prter2  39080  cdleme  40759  rediveud  42640  kelac2lem  43248  frege124d  43944  2ffzoeq  47515  sprsymrelf1lem  47679  paireqne  47699  usgrexmpl2trifr  48225  gpg5grlic  48282  pgnbgreunbgrlem2  48305  mof0ALT  49027  mofsn  49031  f1omoOLD  49081  oppcendc  49205