Theorem eqtr3 2757

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 2747	. 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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  neneor  3032  moeq  3690  euind  3707  reuind  3736  disjeq0  4431  ssprsseq  4801  mosneq  4818  prnebg  4832  prnesn  4836  prel12g  4840  3elpr2eq  4882  eusv1  5361  xpcan  6165  xpcan2  6166  funopg  6570  funopdmsn  7140  funsndifnop  7141  fvf1pr  7300  resf1extb  7930  wfr3g  8321  oawordeulem  8566  nnasmo  8675  en1eqsn  9280  ixpfi2  9362  frr3g  9770  isf32lem2  10368  fpwwe2lem12  10656  1re  11235  receu  11882  xrlttri  13155  injresinjlem  13803  cshwsexaOLD  14843  fsumparts  15822  odd2np1  16360  prmreclem2  16937  divsfval  17561  isprs  18308  psrn  18585  grpinveu  18957  symgextf1  19402  symgfixf1  19418  efgrelexlemb  19731  lspextmo  21014  evlseu  22041  tgcmp  23339  sqf11  27101  dchrisumlem2  27453  sltsolem1  27639  nocvxminlem  27741  divsmo  28139  axlowdimlem15  28935  axcontlem2  28944  wlksoneq1eq2  29644  spthonepeq  29734  uspgrn2crct  29790  wwlksnextinj  29881  frgrwopreglem5lem  30301  numclwwlk1lem2f1  30338  nsnlplig  30462  nsnlpligALT  30463  grpoinveu  30500  5oalem4  31638  rnbra  32088  xreceu  32896  bnj594  34943  bnj953  34970  fnsingle  35937  funimage  35946  funtransport  36049  funray  36158  funline  36160  hilbert1.2  36173  lineintmo  36175  bj-bary1  37330  poimirlem13  37657  poimirlem14  37658  poimirlem17  37661  poimirlem27  37671  antisymressn  38462  disjdmqscossss  38821  prter2  38899  cdleme  40579  kelac2lem  43088  frege124d  43785  2ffzoeq  47356  sprsymrelf1lem  47505  paireqne  47525  usgrexmpl2trifr  48041  gpg5grlic  48093  mof0ALT  48818  mofsn  48822  f1omo  48868  oppcendc  48993