NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  eqtr3i GIF version

Theorem eqtr3i 2375
Description: An equality transitivity inference. (Contributed by NM, 6-May-1994.)
Hypotheses
Ref Expression
eqtr3i.1 A = B
eqtr3i.2 A = C
Assertion
Ref Expression
eqtr3i B = C

Proof of Theorem eqtr3i
StepHypRef Expression
1 eqtr3i.1 . . 3 A = B
21eqcomi 2357 . 2 B = A
3 eqtr3i.2 . 2 A = C
42, 3eqtri 2373 1 B = C
Colors of variables: wff setvar class
Syntax hints:   = wceq 1642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346
This theorem is referenced by:  3eqtr3i  2381  3eqtr3ri  2382  unundi  3424  unundir  3425  inindi  3472  inindir  3473  dfin4  3495  difun1  3514  difabs  3518  notab  3525  dfrab2  3530  dif0  3620  difdifdir  3637  tpidm13  3822  intmin2  3953  compl0  4071  1cnnc  4408  tfinltfinlem1  4500  evenodddisj  4516  sfinltfin  4535  iunxpconst  4819  opabbi2i  4866  dmres  4986  opabresid  5003  rnresi  5011  resdmres  5078  coires1  5096  cnvtr  5098  fcoi1  5240  fopabsn  5441  fvsnun1  5447  funiunfv  5467  caov31  5637  oprabbi2i  5647  mpt2mpt  5709  composefn  5818  braddcfn  5826  frds  5935  enpw1  6062  nncdiv3  6277  nnc3n3p1  6278
  Copyright terms: Public domain W3C validator