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

Theorem eqtr3 2847
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 2831 . 2 (𝐵 = 𝐶𝐶 = 𝐵)
2 eqtr 2845 . 2 ((𝐴 = 𝐶𝐶 = 𝐵) → 𝐴 = 𝐵)
31, 2sylan2b 593 1 ((𝐴 = 𝐶𝐵 = 𝐶) → 𝐴 = 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2116  ax-ext 2796
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1774  df-cleq 2817
This theorem is referenced by:  neneor  3122  moeq  3701  euind  3718  reuind  3747  disjeq0  4407  ssprsseq  4756  mosneq  4771  prnebg  4784  prnesn  4788  prel12g  4792  3elpr2eq  4835  eusv1  5287  xpcan  6030  xpcan2  6031  funopg  6385  foco  6598  funopdmsn  6907  funsndifnop  6908  mpofun  7269  wfr3g  7947  oawordeulem  8173  ixpfi2  8814  isf32lem2  9768  fpwwe2lem13  10056  1re  10633  receu  11277  xrlttri  12525  injresinjlem  13150  cshwsexa  14179  fsumparts  15153  odd2np1  15682  prmreclem2  16245  divsfval  16812  isprs  17532  psrn  17811  grpinveu  18070  symgextf1  18471  symgfixf1  18487  efgrelexlemb  18798  lspextmo  19750  evlseu  20216  tgcmp  21925  sqf11  25630  dchrisumlem2  25980  axlowdimlem15  26657  axcontlem2  26666  wlksoneq1eq2  27361  spthonepeq  27448  uspgrn2crct  27501  wwlksnextinj  27592  frgrwopreglem5lem  28014  numclwwlk1lem2f1  28051  nsnlplig  28173  nsnlpligALT  28174  grpoinveu  28211  5oalem4  29349  rnbra  29799  xreceu  30513  bnj594  32071  bnj953  32098  frr3g  33006  sltsolem1  33065  nocvxminlem  33132  fnsingle  33265  funimage  33274  funtransport  33377  funray  33486  funline  33488  hilbert1.2  33501  lineintmo  33503  bj-bary1  34469  poimirlem13  34773  poimirlem14  34774  poimirlem17  34777  poimirlem27  34787  prter2  35885  cdleme  37564  kelac2lem  39526  frege124d  39968  2ffzoeq  43391  sprsymrelf1lem  43482  paireqne  43502
  Copyright terms: Public domain W3C validator