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

Theorem 3eqtri 2107
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 2103 . 2 𝐵 = 𝐷
51, 4eqtri 2103 1 𝐴 = 𝐷
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 2065
This theorem depends on definitions:  df-bi 115  df-cleq 2076
This theorem is referenced by:  csbid  2924  un23  3141  in32  3194  dfrab2  3255  difun2  3338  tpidm23  3511  unisn  3637  dfiunv2  3734  uniop  4038  suc0  4194  unisuc  4196  iunsuc  4203  xpun  4447  dfrn2  4571  dfdmf  4576  dfrnf  4623  res0  4664  resres  4672  xpssres  4693  dfima2  4720  imai  4731  ima0  4734  imaundir  4787  xpima1  4817  xpima2m  4818  dmresv  4829  rescnvcnv  4833  dmtpop  4846  rnsnopg  4849  resdmres  4862  dmmpt  4866  dmco  4879  co01  4885  fpr  5398  fmptpr  5408  fvsnun2  5414  mpt20  5626  dmoprab  5637  rnoprab  5639  ov6g  5690  1st0  5823  2nd0  5824  dfmpt2  5896  algrflem  5902  dftpos2  5931  tposoprab  5950  tposmpt2  5951  tfrlem8  5988  frecsuc  6077  df2o3  6099  sup00  6511  axi2m1  7173  2p2e4  8296  numsuc  8641  numsucc  8667  decmul10add  8696  5p5e10  8698  6p4e10  8699  7p3e10  8702  xnegmnf  9042  fz0tp  9282  fzo0to2pr  9374  fzo0to3tp  9375  fzo0to42pr  9376  i4  9744  fac1  9823  fac3  9826  abs0  10163  absi  10164  3dvdsdec  10490  3dvds2dec  10491  3lcm2e6woprm  10693  6lcm4e12  10694
  Copyright terms: Public domain W3C validator