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

Theorem eqtr3 2431
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 2414 . 2  |-  ( B  =  C  <->  C  =  B )
2 eqtr 2429 . 2  |-  ( ( A  =  C  /\  C  =  B )  ->  A  =  B )
31, 2sylan2b 462 1  |-  ( ( A  =  C  /\  B  =  C )  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    = wceq 1649
This theorem is referenced by:  eueq  3074  euind  3089  reuind  3105  prnebg  3947  preqsn  3948  eusv1  4684  xpcan  5272  xpcan2  5273  funopg  5452  foco  5630  mpt2fun  6139  oawordeulem  6764  ixpfi2  7371  wemapso2  7485  isf32lem2  8198  fpwwe2lem13  8481  1re  9054  receu  9631  xrlttri  10696  injresinjlem  11162  fsumparts  12548  odd2np1  12871  prmreclem2  13248  divsfval  13735  isprs  14350  psrn  14604  grpinveu  14802  efgrelexlemb  15345  lspextmo  16095  tgcmp  17426  evlseu  19898  sqf11  20883  dchrisumlem2  21145  nbgraf1olem1  21412  spthonepeq  21548  usgrcyclnl2  21589  4cycl4dv  21615  grpoinveu  21771  5oalem4  23120  rnbra  23571  xreceu  24129  wfr3g  25477  frr3g  25502  sltsolem1  25544  nocvxminlem  25566  fnsingle  25680  funimage  25689  axlowdimlem15  25807  axcontlem2  25816  funtransport  25877  funray  25986  funline  25988  hilbert1.2  26001  lineintmo  26003  prtlem11  26613  prter2  26628  kelac2lem  27038  bnj594  29001  bnj953  29028  cdleme  31054
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-an 361  df-ex 1548  df-cleq 2405
  Copyright terms: Public domain W3C validator