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

Theorem 3eqtri 2165
Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
Hypotheses
Ref Expression
3eqtri.1 𝐴 = 𝐵
3eqtri.2 𝐵 = 𝐶
3eqtri.3 𝐶 = 𝐷
Assertion
Ref Expression
3eqtri 𝐴 = 𝐷

Proof of Theorem 3eqtri
StepHypRef Expression
1 3eqtri.1 . 2 𝐴 = 𝐵
2 3eqtri.2 . . 3 𝐵 = 𝐶
3 3eqtri.3 . . 3 𝐶 = 𝐷
42, 3eqtri 2161 . 2 𝐵 = 𝐷
51, 4eqtri 2161 1 𝐴 = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1332
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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-cleq 2133
This theorem is referenced by:  csbid  3014  un23  3239  in32  3292  dfrab2  3355  difun2  3446  tpidm23  3631  unisn  3759  dfiunv2  3856  uniop  4184  suc0  4340  unisuc  4342  iunsuc  4349  xpun  4607  dfrn2  4734  dfdmf  4739  dfrnf  4787  res0  4830  resres  4838  xpssres  4861  dfima2  4890  imai  4902  ima0  4905  imaundir  4959  xpima1  4992  xpima2m  4993  dmresv  5004  rescnvcnv  5008  dmtpop  5021  rnsnopg  5024  resdmres  5037  dmmpt  5041  dmco  5054  co01  5060  fpr  5609  fmptpr  5619  fvsnun2  5625  mpo0  5848  dmoprab  5859  rnoprab  5861  ov6g  5915  1st0  6049  2nd0  6050  dfmpo  6127  algrflem  6133  dftpos2  6165  tposoprab  6184  tposmpo  6185  tfrlem8  6222  frecsuc  6311  df2o3  6334  sbthlemi5  6856  sup00  6897  casedm  6978  djudm  6997  axi2m1  7706  2p2e4  8870  numsuc  9218  numsucc  9244  decmul10add  9273  5p5e10  9275  6p4e10  9276  7p3e10  9279  xnegmnf  9641  pnfaddmnf  9662  fz0tp  9931  fzo0to2pr  10025  fzo0to3tp  10026  fzo0to42pr  10027  0tonninf  10242  1tonninf  10243  inftonninf  10244  sq4e2t8  10420  i4  10425  fac1  10506  fac3  10509  abs0  10861  absi  10862  trirecip  11301  geoihalfsum  11322  esum  11403  tan0  11472  ef01bndlem  11497  3dvdsdec  11596  3dvds2dec  11597  3lcm2e6woprm  11801  6lcm4e12  11802  ennnfonelem1  11954  ndxarg  12019  setsfun  12031  setsfun0  12032  txbasval  12473  cnmpt1st  12494  cnmpt2nd  12495  dvmptidcn  12884  cos2pi  12931  tan4thpi  12968  sincos6thpi  12969  sqrt2cxp2logb9e3  13098  012of  13361  2o01f  13362  pwf1oexmid  13365  isomninnlem  13398  iswomninnlem  13415  ismkvnnlem  13417
  Copyright terms: Public domain W3C validator