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

Theorem eqtr 2448
Description: Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)
Assertion
Ref Expression
eqtr  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )

Proof of Theorem eqtr
StepHypRef Expression
1 eqeq1 2426 . 2  |-  ( A  =  B  ->  ( A  =  C  <->  B  =  C ) )
21biimpar 487 1  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2414
This theorem is referenced by:  eqtr2  2449  eqtr3  2450  sylan9eq  2483  eqvinc  3198  uneqdifeq  3884  preqsn  4180  relresfld  5377  relcoi1OLD  5380  unixpid  5386  eqer  7400  xpider  7438  undifixp  7562  wemaplem2  8064  infeq5  8144  ficard  8990  winalim2  9121  addlsub  10038  pospo  16206  istos  16268  symg2bas  17026  dmatmul  19508  usgra2adedgspthlem2  25325  usgra2wlkspthlem1  25332  rngodm1dm2  26131  rngoidmlem  26136  rngo1cl  26142  rngoueqz  26143  zerdivemp1  26147  eqvincg  28093  bnj545  29701  bnj934  29741  bnj953  29745  poseq  30485  soseq  30486  ordcmp  31099  bj-bary1lem1  31667  poimirlem26  31879  heicant  31888  ismblfin  31894  volsupnfl  31898  itg2addnclem2  31907  itg2addnc  31909  zerdivemp1x  32107  dvheveccl  34598  rp-isfinite5  36081  relexpxpmin  36168  propeqop  38703  usgr2edg  38913
  Copyright terms: Public domain W3C validator