MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqtr3 Structured version   Visualization version   GIF version

Theorem eqtr3 2786
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.)
Assertion
Ref Expression
eqtr3 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)

Proof of Theorem eqtr3
StepHypRef Expression
1 eqcom 2772 . 2 (𝐵 = 𝐶𝐶 = 𝐵)
2 eqtr 2784 . 2 ((𝐴 = 𝐶𝐶 = 𝐵) → 𝐴 = 𝐵)
31, 2sylan2b 587 1 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384   = wceq 1652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758
This theorem is referenced by:  neneor  3036  moeq  3535  eueqOLD  3537  euind  3552  reuind  3572  disjeq0  4184  ssprsseq  4510  mosneq  4525  prnebg  4540  prnesn  4545  prel12g  4550  3elpr2eq  4593  eusv1  5026  xpcan  5753  xpcan2  5754  funopg  6102  foco  6308  funopdmsn  6607  funsndifnop  6608  mpt2fun  6960  wfr3g  7616  oawordeulem  7839  ixpfi2  8471  wemapso2lem  8664  isf32lem2  9429  fpwwe2lem13  9717  1re  10293  receu  10926  xrlttri  12172  injresinjlem  12796  cshwsexa  13855  fsumparts  14824  odd2np1  15349  prmreclem2  15902  divsfval  16475  isprs  17198  psrn  17477  grpinveu  17725  symgextf1  18106  symgfixf1  18122  efgrelexlemb  18429  lspextmo  19328  evlseu  19789  tgcmp  21484  sqf11  25156  dchrisumlem2  25470  axlowdimlem15  26127  axcontlem2  26136  wlksoneq1eq2  26851  spthonepeq  26939  uspgrn2crct  26992  wwlksnextinj  27099  frgrwopreglem5lem  27558  numclwwlk1lem2f1  27599  nsnlplig  27727  nsnlpligALT  27728  grpoinveu  27765  5oalem4  28907  rnbra  29357  xreceu  30012  bnj594  31362  bnj953  31389  frr3g  32155  sltsolem1  32202  nocvxminlem  32269  fnsingle  32402  funimage  32411  funtransport  32514  funray  32623  funline  32625  hilbert1.2  32638  lineintmo  32640  bj-bary1  33528  poimirlem13  33778  poimirlem14  33779  poimirlem17  33782  poimirlem27  33792  prtlem11  34754  prter2  34769  cdleme  36448  kelac2lem  38243  frege124d  38660  2ffzoeq  42004  sprsymrelf1lem  42342
  Copyright terms: Public domain W3C validator