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

Theorem eqtr3i 2104
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 2086 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2102 1  |-  B  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  3eqtr3i  2110  3eqtr3ri  2111  unundi  3134  unundir  3135  inindi  3190  inindir  3191  difun1  3231  difabs  3235  notab  3241  dfrab2  3246  dif0  3321  difdifdirss  3334  tpidm13  3500  intmin2  3670  univ  4233  iunxpconst  4426  dmres  4660  opabresid  4689  rnresi  4712  cnvcnv  4803  rnresv  4810  cnvsn0  4819  cnvsn  4833  resdmres  4842  coi2  4867  coires1  4868  dfdm2  4882  isarep2  5017  ssimaex  5266  fnreseql  5309  fmptpr  5387  idref  5428  mpt2mpt  5627  caov31  5721  xpexgALT  5791  cnvoprab  5886  frec0g  6046  unfiin  6444  halfnqq  6662  caucvgprlemm  6920  caucvgprprlemmu  6947  caucvgsr  7040  mvlladdi  7393  8th4div3  8317  nneoor  8530  nummac  8602  numadd  8604  numaddc  8605  nummul1c  8606  decbin0  8697  infrenegsupex  8763  iseqvalcbv  9531  m1expcl2  9595  facnn  9751  fac0  9752  4bc3eq4  9797  sizeeq0  9818  resqrexlemcalc1  10038  sqrt1  10070  sqrt4  10071  sqrt9  10072  flodddiv4  10478  2prm  10653  znnen  10709
  Copyright terms: Public domain W3C validator