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

Theorem eqtr3i 2162
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 2143 . 2  |-  B  =  A
3 eqtr3i.2 . 2  |-  A  =  C
42, 3eqtri 2160 1  |-  B  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  3eqtr3i  2168  3eqtr3ri  2169  unundi  3237  unundir  3238  inindi  3293  inindir  3294  difun1  3336  difabs  3340  notab  3346  dfrab2  3351  dif0  3433  difdifdirss  3447  tpidm13  3623  intmin2  3797  univ  4397  iunxpconst  4599  dmres  4840  opabresid  4872  rnresi  4896  cnvcnv  4991  rnresv  4998  cnvsn0  5007  cnvsn  5021  resdmres  5030  coi2  5055  coires1  5056  dfdm2  5073  isarep2  5210  ssimaex  5482  fnreseql  5530  fmptpr  5612  idref  5658  mpompt  5863  caov31  5960  xpexgALT  6031  cnvoprab  6131  frec0g  6294  unfiin  6814  xpfi  6818  endjusym  6981  halfnqq  7230  caucvgprlemm  7488  caucvgprprlemmu  7515  caucvgsr  7622  mvlladdi  7992  8th4div3  8951  nneoor  9165  nummac  9238  numadd  9240  numaddc  9241  nummul1c  9242  decbin0  9333  infrenegsupex  9401  iseqvalcbv  10242  m1expcl2  10327  facnn  10485  fac0  10486  4bc3eq4  10531  fihasheq0  10552  resqrexlemcalc1  10798  sqrt1  10830  sqrt4  10831  sqrt9  10832  infxrnegsupex  11044  isumss2  11174  geo2sum2  11296  geoihalfsum  11303  sin0  11447  efival  11450  ef01bndlem  11474  cos2bnd  11478  sin4lt0  11484  flodddiv4  11642  2prm  11819  znnen  11922  ennnfonelemhf1o  11937  setsslid  12023  metreslem  12563  retopbas  12706  sinhalfpilem  12894  sincos6thpi  12945  sincos3rdpi  12946
  Copyright terms: Public domain W3C validator