Theorem eqtr3 2787

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  neneor  3062  moeq  3672  euind  3689  reuind  3718  disjeq0  4416  ssprsseq  4793  mosneq  4809  prnebg  4823  prnesn  4827  prel12g  4831  3elpr2eq  4873  eusv1  5364  axprglem  5409  xpcan  6176  xpcan2  6177  funopg  6574  funopdmsn  7153  funsndifnop  7154  fvf1pr  7314  resf1extb  7937  wfr3g  8322  oawordeulem  8545  nnasmo  8655  en1eqsn  9242  ixpfi2  9314  frr3g  9735  isf32lem2  10353  fpwwe2lem12  10644  1re  11225  receu  11876  xrlttri  13182  injresinjlem  13838  fsumparts  15883  odd2np1  16423  prmreclem2  17001  divsfval  17625  isprs  18376  psrn  18655  grpinveu  19087  symgextf1  19537  symgfixf1  19553  efgrelexlemb  19866  lspextmo  21229  evlseu  22286  tgcmp  23610  sqf11  27356  dchrisumlem2  27707  ltssolem1  27892  nocvxminlem  28000  divsmo  28430  axlowdimlem15  29363  axcontlem2  29372  wlksoneq1eq2  30072  spthonepeq  30167  uspgrn2crct  30226  wwlksnextinj  30317  frgrwopreglem5lem  30744  numclwwlk1lem2f1  30781  nsnlplig  30906  nsnlpligALT  30907  grpoinveu  30944  5oalem4  32082  rnbra  32532  xreceu  33313  bnj594  35367  bnj953  35394  scottsn  35579  fnsingle  36448  funimage  36457  funtransport  36562  funray  36671  funline  36673  hilbert1.2  36686  lineintmo  36688  bj-bary1  38015  poimirlem13  38343  poimirlem14  38344  poimirlem17  38347  poimirlem27  38357  mopre  39180  sucmapleftuniq  39199  antisymressn  39243  disjdmqscossss  39615  prter2  39715  cdleme  41394  rediveud  43264  kelac2lem  43851  frege124d  44547  2ffzoeq  48125  sprsymrelf1lem  48300  paireqne  48320  usgrexmpl2trifr  48862  gpg5grlic  48919  pgnbgreunbgrlem2  48942  mof0ALT  49677  mofsn  49681  f1omoOLD  49731  oppcendc  49855