Theorem eqtr3 2751

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 2741	. 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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  neneor  3025  moeq  3675  euind  3692  reuind  3721  disjeq0  4415  ssprsseq  4785  mosneq  4802  prnebg  4816  prnesn  4820  prel12g  4824  3elpr2eq  4866  eusv1  5341  xpcan  6137  xpcan2  6138  funopg  6534  funopdmsn  7104  funsndifnop  7105  fvf1pr  7264  resf1extb  7890  wfr3g  8275  oawordeulem  8495  nnasmo  8604  en1eqsn  9195  ixpfi2  9277  frr3g  9685  isf32lem2  10283  fpwwe2lem12  10571  1re  11150  receu  11799  xrlttri  13075  injresinjlem  13724  cshwsexaOLD  14766  fsumparts  15748  odd2np1  16287  prmreclem2  16864  divsfval  17486  isprs  18233  psrn  18510  grpinveu  18882  symgextf1  19327  symgfixf1  19343  efgrelexlemb  19656  lspextmo  20939  evlseu  21966  tgcmp  23264  sqf11  27025  dchrisumlem2  27377  sltsolem1  27563  nocvxminlem  27665  divsmo  28063  axlowdimlem15  28859  axcontlem2  28868  wlksoneq1eq2  29566  spthonepeq  29655  uspgrn2crct  29711  wwlksnextinj  29802  frgrwopreglem5lem  30222  numclwwlk1lem2f1  30259  nsnlplig  30383  nsnlpligALT  30384  grpoinveu  30421  5oalem4  31559  rnbra  32009  xreceu  32815  bnj594  34875  bnj953  34902  fnsingle  35880  funimage  35889  funtransport  35992  funray  36101  funline  36103  hilbert1.2  36116  lineintmo  36118  bj-bary1  37273  poimirlem13  37600  poimirlem14  37601  poimirlem17  37604  poimirlem27  37614  antisymressn  38408  disjdmqscossss  38768  prter2  38847  cdleme  40527  rediveud  42404  kelac2lem  43026  frege124d  43723  2ffzoeq  47301  sprsymrelf1lem  47465  paireqne  47485  usgrexmpl2trifr  48001  gpg5grlic  48057  pgnbgreunbgrlem2  48080  mof0ALT  48801  mofsn  48805  f1omoOLD  48855  oppcendc  48980