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

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

Proof of Theorem eqtr3i
StepHypRef Expression
1 eqtr3i.1 . . 3 𝐴 = 𝐵
21eqcomi 2119 . 2 𝐵 = 𝐴
3 eqtr3i.2 . 2 𝐴 = 𝐶
42, 3eqtri 2135 1 𝐵 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1314
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-cleq 2108
This theorem is referenced by:  3eqtr3i  2143  3eqtr3ri  2144  unundi  3203  unundir  3204  inindi  3259  inindir  3260  difun1  3302  difabs  3306  notab  3312  dfrab2  3317  dif0  3399  difdifdirss  3413  tpidm13  3589  intmin2  3763  univ  4357  iunxpconst  4559  dmres  4798  opabresid  4830  rnresi  4854  cnvcnv  4949  rnresv  4956  cnvsn0  4965  cnvsn  4979  resdmres  4988  coi2  5013  coires1  5014  dfdm2  5031  isarep2  5168  ssimaex  5436  fnreseql  5484  fmptpr  5566  idref  5612  mpompt  5817  caov31  5914  xpexgALT  5985  cnvoprab  6085  frec0g  6248  unfiin  6767  xpfi  6771  endjusym  6933  halfnqq  7166  caucvgprlemm  7424  caucvgprprlemmu  7451  caucvgsr  7544  mvlladdi  7903  8th4div3  8843  nneoor  9057  nummac  9130  numadd  9132  numaddc  9133  nummul1c  9134  decbin0  9225  infrenegsupex  9291  iseqvalcbv  10123  m1expcl2  10208  facnn  10366  fac0  10367  4bc3eq4  10412  fihasheq0  10433  resqrexlemcalc1  10678  sqrt1  10710  sqrt4  10711  sqrt9  10712  infxrnegsupex  10924  isumss2  11054  geo2sum2  11176  geoihalfsum  11183  sin0  11287  efival  11290  ef01bndlem  11314  cos2bnd  11318  sin4lt0  11324  flodddiv4  11479  2prm  11654  znnen  11756  ennnfonelemhf1o  11771  setsslid  11852  metreslem  12369  retopbas  12512
  Copyright terms: Public domain W3C validator