Theorem eqtr3 2784

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754

This theorem is referenced by:  neneor  3057  moeq  3670  euind  3687  reuind  3716  disjeq0  4410  ssprsseq  4783  mosneq  4800  prnebg  4814  prnesn  4818  prel12g  4822  3elpr2eq  4864  eusv1  5348  axprglem  5393  xpcan  6162  xpcan2  6163  funopg  6555  funopdmsn  7133  funsndifnop  7134  fvf1pr  7291  resf1extb  7915  wfr3g  8300  oawordeulem  8523  nnasmo  8633  en1eqsn  9219  ixpfi2  9293  frr3g  9714  isf32lem2  10311  fpwwe2lem12  10600  1re  11181  receu  11832  xrlttri  13141  injresinjlem  13796  fsumparts  15834  odd2np1  16375  prmreclem2  16953  divsfval  17577  isprs  18328  psrn  18607  grpinveu  19016  symgextf1  19461  symgfixf1  19477  efgrelexlemb  19790  lspextmo  21120  evlseu  22133  tgcmp  23458  sqf11  27200  dchrisumlem2  27551  ltssolem1  27736  nocvxminlem  27844  divsmo  28274  axlowdimlem15  29154  axcontlem2  29163  wlksoneq1eq2  29860  spthonepeq  29949  uspgrn2crct  30005  wwlksnextinj  30096  frgrwopreglem5lem  30519  numclwwlk1lem2f1  30556  nsnlplig  30681  nsnlpligALT  30682  grpoinveu  30719  5oalem4  31857  rnbra  32307  xreceu  33096  bnj594  35204  bnj953  35231  fnsingle  36264  funimage  36273  funtransport  36378  funray  36487  funline  36489  hilbert1.2  36502  lineintmo  36504  bj-bary1  37801  poimirlem13  38129  poimirlem14  38130  poimirlem17  38133  poimirlem27  38143  mopre  38967  sucmapleftuniq  38986  antisymressn  39030  disjdmqscossss  39402  prter2  39502  cdleme  41181  rediveud  43049  kelac2lem  43638  frege124d  44334  2ffzoeq  47919  sprsymrelf1lem  48094  paireqne  48114  usgrexmpl2trifr  48656  gpg5grlic  48713  pgnbgreunbgrlem2  48736  mof0ALT  49458  mofsn  49462  f1omoOLD  49512  oppcendc  49636