Theorem eqtr3 2758

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

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

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  neneor  3032  moeq  3653  euind  3670  reuind  3699  disjeq0  4396  ssprsseq  4768  mosneq  4785  prnebg  4799  prnesn  4803  prel12g  4807  3elpr2eq  4849  eusv1  5333  axprglem  5378  xpcan  6140  xpcan2  6141  funopg  6532  funopdmsn  7104  funsndifnop  7105  fvf1pr  7262  resf1extb  7885  wfr3g  8269  oawordeulem  8489  nnasmo  8599  en1eqsn  9185  ixpfi2  9260  frr3g  9680  isf32lem2  10276  fpwwe2lem12  10565  1re  11144  receu  11795  xrlttri  13090  injresinjlem  13745  fsumparts  15769  odd2np1  16310  prmreclem2  16888  divsfval  17511  isprs  18262  psrn  18541  grpinveu  18950  symgextf1  19396  symgfixf1  19412  efgrelexlemb  19725  lspextmo  21051  evlseu  22061  tgcmp  23366  sqf11  27102  dchrisumlem2  27453  ltssolem1  27639  nocvxminlem  27746  divsmo  28176  axlowdimlem15  29025  axcontlem2  29034  wlksoneq1eq2  29731  spthonepeq  29820  uspgrn2crct  29876  wwlksnextinj  29967  frgrwopreglem5lem  30390  numclwwlk1lem2f1  30427  nsnlplig  30552  nsnlpligALT  30553  grpoinveu  30590  5oalem4  31728  rnbra  32178  xreceu  32981  bnj594  35054  bnj953  35081  fnsingle  36099  funimage  36108  funtransport  36213  funray  36322  funline  36324  hilbert1.2  36337  lineintmo  36339  bj-bary1  37626  poimirlem13  37954  poimirlem14  37955  poimirlem17  37958  poimirlem27  37968  mopre  38792  sucmapleftuniq  38811  antisymressn  38855  disjdmqscossss  39227  prter2  39327  cdleme  41006  rediveud  42875  kelac2lem  43492  frege124d  44188  2ffzoeq  47776  sprsymrelf1lem  47951  paireqne  47971  usgrexmpl2trifr  48513  gpg5grlic  48570  pgnbgreunbgrlem2  48593  mof0ALT  49315  mofsn  49319  f1omoOLD  49369  oppcendc  49493