Theorem eqtr3 2759

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

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  neneor  3043  moeq  3704  euind  3721  reuind  3750  disjeq0  4456  ssprsseq  4829  mosneq  4844  prnebg  4857  prnesn  4861  prel12g  4865  3elpr2eq  4908  eusv1  5390  xpcan  6176  xpcan2  6177  funopg  6583  funopdmsn  7148  funsndifnop  7149  mpofunOLD  7533  wfr3g  8307  oawordeulem  8554  nnasmo  8662  en1eqsn  9274  ixpfi2  9350  frr3g  9751  isf32lem2  10349  fpwwe2lem12  10637  1re  11214  receu  11859  xrlttri  13118  injresinjlem  13752  cshwsexaOLD  14775  fsumparts  15752  odd2np1  16284  prmreclem2  16850  divsfval  17493  isprs  18250  psrn  18528  grpinveu  18859  symgextf1  19289  symgfixf1  19305  efgrelexlemb  19618  lspextmo  20667  evlseu  21646  tgcmp  22905  sqf11  26643  dchrisumlem2  26993  sltsolem1  27178  nocvxminlem  27279  divsmo  27634  axlowdimlem15  28214  axcontlem2  28223  wlksoneq1eq2  28921  spthonepeq  29009  uspgrn2crct  29062  wwlksnextinj  29153  frgrwopreglem5lem  29573  numclwwlk1lem2f1  29610  nsnlplig  29734  nsnlpligALT  29735  grpoinveu  29772  5oalem4  30910  rnbra  31360  xreceu  32088  bnj594  33923  bnj953  33950  fnsingle  34891  funimage  34900  funtransport  35003  funray  35112  funline  35114  hilbert1.2  35127  lineintmo  35129  bj-bary1  36193  poimirlem13  36501  poimirlem14  36502  poimirlem17  36505  poimirlem27  36515  antisymressn  37314  disjdmqscossss  37673  prter2  37751  cdleme  39431  kelac2lem  41806  frege124d  42512  2ffzoeq  46036  sprsymrelf1lem  46159  paireqne  46179  mof0ALT  47506  mofsn  47510  f1omo  47527