Theorem eqtr3 2759

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 2749	. 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 2709

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

This theorem is referenced by:  neneor  3033  moeq  3667  euind  3684  reuind  3713  disjeq0  4410  ssprsseq  4783  mosneq  4800  prnebg  4814  prnesn  4818  prel12g  4822  3elpr2eq  4864  eusv1  5338  axprglem  5382  xpcan  6142  xpcan2  6143  funopg  6534  funopdmsn  7105  funsndifnop  7106  fvf1pr  7263  resf1extb  7886  wfr3g  8271  oawordeulem  8491  nnasmo  8601  en1eqsn  9187  ixpfi2  9262  frr3g  9680  isf32lem2  10276  fpwwe2lem12  10565  1re  11144  receu  11794  xrlttri  13065  injresinjlem  13718  fsumparts  15741  odd2np1  16280  prmreclem2  16857  divsfval  17480  isprs  18231  psrn  18510  grpinveu  18916  symgextf1  19362  symgfixf1  19378  efgrelexlemb  19691  lspextmo  21020  evlseu  22050  tgcmp  23357  sqf11  27117  dchrisumlem2  27469  ltssolem1  27655  nocvxminlem  27762  divsmo  28192  axlowdimlem15  29041  axcontlem2  29050  wlksoneq1eq2  29748  spthonepeq  29837  uspgrn2crct  29893  wwlksnextinj  29984  frgrwopreglem5lem  30407  numclwwlk1lem2f1  30444  nsnlplig  30569  nsnlpligALT  30570  grpoinveu  30607  5oalem4  31745  rnbra  32195  xreceu  33014  bnj594  35088  bnj953  35115  fnsingle  36133  funimage  36142  funtransport  36247  funray  36356  funline  36358  hilbert1.2  36371  lineintmo  36373  bj-bary1  37567  poimirlem13  37884  poimirlem14  37885  poimirlem17  37888  poimirlem27  37898  mopre  38722  sucmapleftuniq  38741  antisymressn  38785  disjdmqscossss  39157  prter2  39257  cdleme  40936  rediveud  42813  kelac2lem  43421  frege124d  44117  2ffzoeq  47687  sprsymrelf1lem  47851  paireqne  47871  usgrexmpl2trifr  48397  gpg5grlic  48454  pgnbgreunbgrlem2  48477  mof0ALT  49199  mofsn  49203  f1omoOLD  49253  oppcendc  49377