Theorem eqtr3 2763

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 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 2708

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

This theorem is referenced by:  neneor  3042  moeq  3713  euind  3730  reuind  3759  disjeq0  4456  ssprsseq  4825  mosneq  4842  prnebg  4856  prnesn  4860  prel12g  4864  3elpr2eq  4906  eusv1  5391  xpcan  6196  xpcan2  6197  funopg  6600  funopdmsn  7170  funsndifnop  7171  fvf1pr  7327  resf1extb  7956  wfr3g  8347  oawordeulem  8592  nnasmo  8701  en1eqsn  9308  ixpfi2  9390  frr3g  9796  isf32lem2  10394  fpwwe2lem12  10682  1re  11261  receu  11908  xrlttri  13181  injresinjlem  13826  cshwsexaOLD  14863  fsumparts  15842  odd2np1  16378  prmreclem2  16955  divsfval  17592  isprs  18342  psrn  18620  grpinveu  18992  symgextf1  19439  symgfixf1  19455  efgrelexlemb  19768  lspextmo  21055  evlseu  22107  tgcmp  23409  sqf11  27182  dchrisumlem2  27534  sltsolem1  27720  nocvxminlem  27822  divsmo  28210  axlowdimlem15  28971  axcontlem2  28980  wlksoneq1eq2  29682  spthonepeq  29772  uspgrn2crct  29828  wwlksnextinj  29919  frgrwopreglem5lem  30339  numclwwlk1lem2f1  30376  nsnlplig  30500  nsnlpligALT  30501  grpoinveu  30538  5oalem4  31676  rnbra  32126  xreceu  32904  bnj594  34926  bnj953  34953  fnsingle  35920  funimage  35929  funtransport  36032  funray  36141  funline  36143  hilbert1.2  36156  lineintmo  36158  bj-bary1  37313  poimirlem13  37640  poimirlem14  37641  poimirlem17  37644  poimirlem27  37654  antisymressn  38445  disjdmqscossss  38804  prter2  38882  cdleme  40562  kelac2lem  43076  frege124d  43774  2ffzoeq  47339  sprsymrelf1lem  47478  paireqne  47498  usgrexmpl2trifr  47996  gpg5grlic  48047  mof0ALT  48749  mofsn  48753  f1omo  48792  oppcendc  48906