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

Theorem eqtr3i 2140
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 2121 . 2 𝐵 = 𝐴
3 eqtr3i.2 . 2 𝐴 = 𝐶
42, 3eqtri 2138 1 𝐵 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  3eqtr3i  2146  3eqtr3ri  2147  unundi  3207  unundir  3208  inindi  3263  inindir  3264  difun1  3306  difabs  3310  notab  3316  dfrab2  3321  dif0  3403  difdifdirss  3417  tpidm13  3593  intmin2  3767  univ  4367  iunxpconst  4569  dmres  4810  opabresid  4842  rnresi  4866  cnvcnv  4961  rnresv  4968  cnvsn0  4977  cnvsn  4991  resdmres  5000  coi2  5025  coires1  5026  dfdm2  5043  isarep2  5180  ssimaex  5450  fnreseql  5498  fmptpr  5580  idref  5626  mpompt  5831  caov31  5928  xpexgALT  5999  cnvoprab  6099  frec0g  6262  unfiin  6782  xpfi  6786  endjusym  6949  halfnqq  7186  caucvgprlemm  7444  caucvgprprlemmu  7471  caucvgsr  7578  mvlladdi  7948  8th4div3  8907  nneoor  9121  nummac  9194  numadd  9196  numaddc  9197  nummul1c  9198  decbin0  9289  infrenegsupex  9357  iseqvalcbv  10198  m1expcl2  10283  facnn  10441  fac0  10442  4bc3eq4  10487  fihasheq0  10508  resqrexlemcalc1  10754  sqrt1  10786  sqrt4  10787  sqrt9  10788  infxrnegsupex  11000  isumss2  11130  geo2sum2  11252  geoihalfsum  11259  sin0  11363  efival  11366  ef01bndlem  11390  cos2bnd  11394  sin4lt0  11400  flodddiv4  11558  2prm  11735  znnen  11838  ennnfonelemhf1o  11853  setsslid  11936  metreslem  12476  retopbas  12619  sinhalfpilem  12799  sincos6thpi  12850  sincos3rdpi  12851
  Copyright terms: Public domain W3C validator