ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqtr3i Structured version   GIF version

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

Proof of Theorem eqtr3i
StepHypRef Expression
1 eqtr3i.1 . . 3 A = B
21eqcomi 2041 . 2 B = A
3 eqtr3i.2 . 2 A = 𝐶
42, 3eqtri 2057 1 B = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  3eqtr3i  2065  3eqtr3ri  2066  unundi  3098  unundir  3099  inindi  3148  inindir  3149  difun1  3191  difabs  3195  notab  3201  dfrab2  3206  dif0  3288  difdifdirss  3301  tpidm13  3461  intmin2  3632  univ  4173  iunxpconst  4343  dmres  4575  opabresid  4602  rnresi  4625  cnvcnv  4716  rnresv  4723  cnvsn0  4732  cnvsn  4746  resdmres  4755  coi2  4780  coires1  4781  dfdm2  4795  isarep2  4929  ssimaex  5177  fnreseql  5220  fmptpr  5298  idref  5339  mpt2mpt  5538  caov31  5632  xpexgALT  5702  frec0g  5922  halfnqq  6393  caucvgprlemm  6639  mvlladdi  7025  8th4div3  7921  nneoor  8116  dec10  8173  nummac  8175  numadd  8177  numaddc  8178  nummul1c  8179  9p2e11  8205  decbin0  8246  m1expcl2  8931  sqrt1  9216  sqrt4  9217  sqrt9  9218
  Copyright terms: Public domain W3C validator