Theorem eqtr3 2751

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 2741	. 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 2701

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

This theorem is referenced by:  neneor  3025  moeq  3678  euind  3695  reuind  3724  disjeq0  4419  ssprsseq  4789  mosneq  4806  prnebg  4820  prnesn  4824  prel12g  4828  3elpr2eq  4870  eusv1  5346  xpcan  6149  xpcan2  6150  funopg  6550  funopdmsn  7122  funsndifnop  7123  fvf1pr  7282  resf1extb  7910  wfr3g  8298  oawordeulem  8518  nnasmo  8627  en1eqsn  9219  ixpfi2  9301  frr3g  9709  isf32lem2  10307  fpwwe2lem12  10595  1re  11174  receu  11823  xrlttri  13099  injresinjlem  13748  cshwsexaOLD  14790  fsumparts  15772  odd2np1  16311  prmreclem2  16888  divsfval  17510  isprs  18257  psrn  18534  grpinveu  18906  symgextf1  19351  symgfixf1  19367  efgrelexlemb  19680  lspextmo  20963  evlseu  21990  tgcmp  23288  sqf11  27049  dchrisumlem2  27401  sltsolem1  27587  nocvxminlem  27689  divsmo  28087  axlowdimlem15  28883  axcontlem2  28892  wlksoneq1eq2  29592  spthonepeq  29682  uspgrn2crct  29738  wwlksnextinj  29829  frgrwopreglem5lem  30249  numclwwlk1lem2f1  30286  nsnlplig  30410  nsnlpligALT  30411  grpoinveu  30448  5oalem4  31586  rnbra  32036  xreceu  32842  bnj594  34902  bnj953  34929  fnsingle  35907  funimage  35916  funtransport  36019  funray  36128  funline  36130  hilbert1.2  36143  lineintmo  36145  bj-bary1  37300  poimirlem13  37627  poimirlem14  37628  poimirlem17  37631  poimirlem27  37641  antisymressn  38435  disjdmqscossss  38795  prter2  38874  cdleme  40554  rediveud  42431  kelac2lem  43053  frege124d  43750  2ffzoeq  47328  sprsymrelf1lem  47492  paireqne  47512  usgrexmpl2trifr  48028  gpg5grlic  48084  pgnbgreunbgrlem2  48107  mof0ALT  48828  mofsn  48832  f1omoOLD  48882  oppcendc  49007