Theorem eqtr 2483

Description: Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13. (Contributed by NM, 25-Jan-2004.)

Assertion

Ref	Expression
eqtr

Proof of Theorem eqtr

Step	Hyp	Ref	Expression
1		eqeq1 2461	. 2
2	1	biimpar 485	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395

This theorem is referenced by:  eqtr2  2484  eqtr3  2485  sylan9eq  2518  eqvinc  3226  uneqdifeq  3916  preqsn  4213  relresfld  5539  relcoi1  5541  unixpid  5547  eqer  7363  xpider  7401  undifixp  7525  wemaplem2  7993  infeq5  8075  ficard  8961  winalim2  9095  uzindOLD  10982  pospo  15603  istos  15665  symg2bas  16423  dmatmul  18999  bwthOLD  19911  usgra2adedgspthlem2  24612  usgra2wlkspthlem1  24619  rngodm1dm2  25420  rngoidmlem  25425  rngo1cl  25431  rngoueqz  25432  zerdivemp1  25436  eqvincg  27374  poseq  29333  soseq  29334  ordcmp  29912  heicant  30049  ismblfin  30055  volsupnfl  30059  itg2addnclem2  30067  itg2addnc  30069  zerdivemp1x  30358  bnj545  33953  bnj934  33993  bnj953  33997  bj-lsub  34671  bj-bary1lem1  34680  dvheveccl  36839  rp-isfinite5  37743

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449