Theorem eqtr 1904

Description: Transitive law for class equality. Proposition 4.7(3) of [TakeutiZaring] p. 13.

Assertion

Ref	Expression
eqtr	|- ((A = B /\ B = C) -> A = C)

Proof of Theorem eqtr

Step	Hyp	Ref	Expression
1		eqeq1 1890	. 2 |- (A = B -> (A = C <-> B = C))
2	1	biimpar 461	1 |- ((A = B /\ B = C) -> A = C)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298

This theorem is referenced by:  eqtr2 1905  eqtr2OLD 1906  eqtr3 1907  sylan9eq 1948  eqvinc 2387  preqsn 3157  iderOLD 5327  eqer 5329  xpmapenlem4 5593  infeq5 5727  cfom 6064  uzindOLD 7420  sn0top 8917  cnconst 9057  gapm 9462  ring2 9474  efif1lem5 10088  twpar2 10149  ficard 10176  cncomp 10331  usinuniop 10341  ismnd2 10392  rnplrnml0 10402  ringidmlem 10409  on1el3 10412  on1el4 10413  ring1cl 10415  uznzr 10416  bnj545 13271  bnj934 13334  bnj953 13343  mulgcdlem2 13757  poseq 13954  soseq 13955  dfoprab4spop 14339  neiopne 14354  oooeqim2 14356  domfldref 14365  fldsqcp2 14378  sqpeq 14383  cmprelid2 14447  resrelfld 14448  injrec 14461  surjsec 14462  fopab2g 14485  injsurinj 14487  repfuntw 14502  cbcpcp 14504  unprj 14511  nZdef 14527  jidd 14540  midd 14541  valcurfn1 14552  preoref22 14570  ubos2 14598  supdef 14604  mxlelt2 14606  mnlelt2 14608  defse3 14614  istoset2 14628  dfps2 14634  isdir2 14640  ridlideq 14695  rzrlzreq 14696  clfsebs2 14710  symgfo 14730  grpdivone 14736  rngmgmbs3 14766  rnplrnml3 14768  zerdivemp1 14785  zintdom 14787  svs2 14829  homcard 14893  subspemp 14903  subtopsin2 14907  cnfilca 14927  limfillem2 14939  limvinlv 14941  bwt2 14960  clindistop 14962  trhom 14983  tpgprop1 14986  tpgprop2 14987  altretop 14997  dualcat2lem 15129  dualded2lem 15130  imonclem 15162  isepic 15173  cptarc 15242  opncldf1 15402  subsubtop 15423  compfipin0lem 15435  compfipin0 15436  fbasfip 15556  filssufil 15571  inficl 15757  phtpycom 16050  phtpyco 16056  phtpcer 16062  zerdivemp1x 16108

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-17 1317  ax-4 1319  ax-5o 1321  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-cleq 1877

Copyright terms: Public domain