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

Theorem 3eqtri 2080
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 2076 . 2 𝐵 = 𝐷
51, 4eqtri 2076 1 𝐴 = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  csbid  2886  un23  3129  in32  3176  dfrab2  3239  difun2  3329  tpidm23  3498  unisn  3623  dfiunv2  3720  uniop  4019  suc0  4175  unisuc  4177  iunsuc  4184  xpun  4428  dfrn2  4550  dfdmf  4555  dfrnf  4602  res0  4643  resres  4651  xpssres  4672  dfima2  4697  imai  4708  ima0  4711  imaundir  4764  xpima1  4794  xpima2m  4795  dmresv  4806  rescnvcnv  4810  dmtpop  4823  rnsnopg  4826  resdmres  4839  dmmpt  4843  dmco  4856  co01  4862  fpr  5372  fmptpr  5382  fvsnun2  5388  mpt20  5601  dmoprab  5612  rnoprab  5614  ov6g  5665  1st0  5798  2nd0  5799  dfmpt2  5871  algrflem  5877  dftpos2  5906  tposoprab  5925  tposmpt2  5926  tfrlem8  5964  df2o3  6044  sup00  6406  axi2m1  7006  2p2e4  8109  numsuc  8439  numsucc  8465  decmul10add  8494  5p5e10  8496  6p4e10  8497  7p3e10  8500  xnegmnf  8842  fz0tp  9082  fzo0to2pr  9175  fzo0to3tp  9176  fzo0to42pr  9177  i4  9520  fac1  9596  fac3  9599  abs0  9884  absi  9885  3dvdsdec  10175  3dvds2dec  10176
  Copyright terms: Public domain W3C validator