Theorem eqtr3 2758

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  neneor  3032  moeq  3665  euind  3682  reuind  3711  disjeq0  4408  ssprsseq  4781  mosneq  4798  prnebg  4812  prnesn  4816  prel12g  4820  3elpr2eq  4862  eusv1  5336  xpcan  6134  xpcan2  6135  funopg  6526  funopdmsn  7095  funsndifnop  7096  fvf1pr  7253  resf1extb  7876  wfr3g  8261  oawordeulem  8481  nnasmo  8591  en1eqsn  9175  ixpfi2  9250  frr3g  9668  isf32lem2  10264  fpwwe2lem12  10553  1re  11132  receu  11782  xrlttri  13053  injresinjlem  13706  fsumparts  15729  odd2np1  16268  prmreclem2  16845  divsfval  17468  isprs  18219  psrn  18498  grpinveu  18904  symgextf1  19350  symgfixf1  19366  efgrelexlemb  19679  lspextmo  21008  evlseu  22038  tgcmp  23345  sqf11  27105  dchrisumlem2  27457  ltssolem1  27643  nocvxminlem  27750  divsmo  28180  axlowdimlem15  29029  axcontlem2  29038  wlksoneq1eq2  29736  spthonepeq  29825  uspgrn2crct  29881  wwlksnextinj  29972  frgrwopreglem5lem  30395  numclwwlk1lem2f1  30432  nsnlplig  30556  nsnlpligALT  30557  grpoinveu  30594  5oalem4  31732  rnbra  32182  xreceu  33003  bnj594  35068  bnj953  35095  fnsingle  36111  funimage  36120  funtransport  36225  funray  36334  funline  36336  hilbert1.2  36349  lineintmo  36351  bj-bary1  37517  poimirlem13  37834  poimirlem14  37835  poimirlem17  37838  poimirlem27  37848  mopre  38645  sucmapleftuniq  38663  antisymressn  38707  disjdmqscossss  39062  prter2  39141  cdleme  40820  rediveud  42698  kelac2lem  43306  frege124d  44002  2ffzoeq  47573  sprsymrelf1lem  47737  paireqne  47757  usgrexmpl2trifr  48283  gpg5grlic  48340  pgnbgreunbgrlem2  48363  mof0ALT  49085  mofsn  49089  f1omoOLD  49139  oppcendc  49263