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

Theorem 3eqtri 2080
Description: An inference from three chained equalities. (Contributed by NM, 29-Aug-1993.)
Hypotheses
Ref Expression
3eqtri.1  |-  A  =  B
3eqtri.2  |-  B  =  C
3eqtri.3  |-  C  =  D
Assertion
Ref Expression
3eqtri  |-  A  =  D

Proof of Theorem 3eqtri
StepHypRef Expression
1 3eqtri.1 . 2  |-  A  =  B
2 3eqtri.2 . . 3  |-  B  =  C
3 3eqtri.3 . . 3  |-  C  =  D
42, 3eqtri 2076 . 2  |-  B  =  D
51, 4eqtri 2076 1  |-  A  =  D
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  2887  un23  3130  in32  3177  dfrab2  3240  difun2  3330  tpidm23  3499  unisn  3624  dfiunv2  3721  uniop  4020  suc0  4176  unisuc  4178  iunsuc  4185  xpun  4429  dfrn2  4551  dfdmf  4556  dfrnf  4603  res0  4644  resres  4652  xpssres  4673  dfima2  4698  imai  4709  ima0  4712  imaundir  4765  xpima1  4795  xpima2m  4796  dmresv  4807  rescnvcnv  4811  dmtpop  4824  rnsnopg  4827  resdmres  4840  dmmpt  4844  dmco  4857  co01  4863  fpr  5373  fmptpr  5383  fvsnun2  5389  mpt20  5602  dmoprab  5613  rnoprab  5615  ov6g  5666  1st0  5799  2nd0  5800  dfmpt2  5872  algrflem  5878  dftpos2  5907  tposoprab  5926  tposmpt2  5927  tfrlem8  5965  df2o3  6045  sup00  6407  axi2m1  7007  2p2e4  8110  numsuc  8440  numsucc  8466  decmul10add  8495  5p5e10  8497  6p4e10  8498  7p3e10  8501  xnegmnf  8843  fz0tp  9083  fzo0to2pr  9176  fzo0to3tp  9177  fzo0to42pr  9178  i4  9521  fac1  9597  fac3  9600  abs0  9885  absi  9886  3dvdsdec  10176  3dvds2dec  10177
  Copyright terms: Public domain W3C validator