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

Theorem eqtr3i 2036
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 2018 . 2 B = A
3 eqtr3i.2 . 2 A = 𝐶
42, 3eqtri 2034 1 B = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1224
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 1310  ax-gen 1312  ax-4 1374  ax-17 1393  ax-ext 1996
This theorem depends on definitions:  df-bi 110  df-cleq 2007
This theorem is referenced by:  3eqtr3i  2042  3eqtr3ri  2043  unundi  3073  unundir  3074  inindi  3123  inindir  3124  difun1  3166  difabs  3170  notab  3176  dfrab2  3181  dif0  3263  difdifdirss  3276  tpidm13  3434  intmin2  3605  univ  4146  iunxpconst  4316  dmres  4548  opabresid  4575  rnresi  4598  cnvcnv  4689  rnresv  4696  cnvsn0  4705  cnvsn  4719  resdmres  4728  coi2  4753  coires1  4754  dfdm2  4768  isarep2  4901  ssimaex  5148  fnreseql  5191  fmptpr  5269  idref  5310  mpt2mpt  5508  caov31  5602  xpexgALT  5672  frec0g  5891  halfnqq  6254  mvlladdi  6829  8th4div3  7723  nneoor  7906  dec10  7962  nummac  7964  numadd  7966  numaddc  7967  nummul1c  7968  9p2e11  7994  decbin0  8035
  Copyright terms: Public domain W3C validator