Theorem eqtr3 2791

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

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  neneor  3066  moeq  3679  euind  3696  reuind  3725  disjeq0  4422  ssprsseq  4795  mosneq  4811  prnebg  4825  prnesn  4829  prel12g  4833  3elpr2eq  4875  eusv1  5363  axprglem  5408  xpcan  6175  xpcan2  6176  funopg  6571  funopdmsn  7148  funsndifnop  7149  fvf1pr  7306  resf1extb  7930  wfr3g  8315  oawordeulem  8538  nnasmo  8648  en1eqsn  9234  ixpfi2  9306  frr3g  9727  isf32lem2  10337  fpwwe2lem12  10626  1re  11207  receu  11858  xrlttri  13163  injresinjlem  13818  fsumparts  15857  odd2np1  16398  prmreclem2  16976  divsfval  17600  isprs  18351  psrn  18630  grpinveu  19040  symgextf1  19490  symgfixf1  19506  efgrelexlemb  19819  lspextmo  21154  evlseu  22202  tgcmp  23526  sqf11  27268  dchrisumlem2  27619  ltssolem1  27804  nocvxminlem  27912  divsmo  28342  axlowdimlem15  29246  axcontlem2  29255  wlksoneq1eq2  29952  spthonepeq  30041  uspgrn2crct  30097  wwlksnextinj  30188  frgrwopreglem5lem  30611  numclwwlk1lem2f1  30648  nsnlplig  30773  nsnlpligALT  30774  grpoinveu  30811  5oalem4  31949  rnbra  32399  xreceu  33181  bnj594  35244  bnj953  35271  fnsingle  36307  funimage  36316  funtransport  36421  funray  36530  funline  36532  hilbert1.2  36545  lineintmo  36547  bj-bary1  37843  poimirlem13  38171  poimirlem14  38172  poimirlem17  38175  poimirlem27  38185  mopre  39009  sucmapleftuniq  39028  antisymressn  39072  disjdmqscossss  39444  prter2  39544  cdleme  41223  rediveud  43093  kelac2lem  43682  frege124d  44378  2ffzoeq  47953  sprsymrelf1lem  48128  paireqne  48148  usgrexmpl2trifr  48690  gpg5grlic  48747  pgnbgreunbgrlem2  48770  mof0ALT  49502  mofsn  49506  f1omoOLD  49556  oppcendc  49680