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

Theorem eqtr3 2457
Description: A transitive law for class equality. (Contributed by NM, 20-May-2005.)
Assertion
Ref Expression
eqtr3  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )

Proof of Theorem eqtr3
StepHypRef Expression
1 eqcom 2440 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2455 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 475 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2431
This theorem is referenced by:  eueq  3126  euind  3141  reuind  3157  prnebg  4049  preqsn  4050  eusv1  4481  restidsing  5157  xpcan  5269  xpcan2  5270  funopg  5445  foco  5625  mpt2fun  6187  oawordeulem  6985  ixpfi2  7601  wemapso2OLD  7758  wemapso2lem  7759  isf32lem2  8515  fpwwe2lem13  8801  1re  9377  receu  9973  xrlttri  11108  injresinjlem  11630  hash2prd  12173  cshwsexa  12450  fsumparts  13261  odd2np1  13584  prmreclem2  13970  divsfval  14477  isprs  15092  psrn  15371  grpinveu  15563  symgextf1  15917  symgfixf1  15934  efgrelexlemb  16238  lspextmo  17114  evlseu  17577  tgcmp  18979  sqf11  22452  dchrisumlem2  22714  axlowdimlem15  23153  axcontlem2  23162  nbgraf1olem1  23301  spthonepeq  23437  usgrcyclnl2  23478  4cycl4dv  23504  grpoinveu  23660  5oalem4  25011  rnbra  25462  xreceu  26048  wfr3g  27674  frr3g  27718  sltsolem1  27760  nocvxminlem  27782  fnsingle  27901  funimage  27910  funtransport  28013  funray  28122  funline  28124  hilbert1.2  28137  lineintmo  28139  prtlem11  28964  prter2  28979  kelac2lem  29370  2ffzoeq  30167  wwlkextinj  30315  numclwlk1lem2f1  30640  bnj594  31792  bnj953  31819  bj-bary1  32443  cdleme  34044
  Copyright terms: Public domain W3C validator