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

Theorem 3eqtri 2164
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 2160 . 2  |-  B  =  D
51, 4eqtri 2160 1  |-  A  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1331
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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  csbid  3011  un23  3235  in32  3288  dfrab2  3351  difun2  3442  tpidm23  3624  unisn  3752  dfiunv2  3849  uniop  4177  suc0  4333  unisuc  4335  iunsuc  4342  xpun  4600  dfrn2  4727  dfdmf  4732  dfrnf  4780  res0  4823  resres  4831  xpssres  4854  dfima2  4883  imai  4895  ima0  4898  imaundir  4952  xpima1  4985  xpima2m  4986  dmresv  4997  rescnvcnv  5001  dmtpop  5014  rnsnopg  5017  resdmres  5030  dmmpt  5034  dmco  5047  co01  5053  fpr  5602  fmptpr  5612  fvsnun2  5618  mpo0  5841  dmoprab  5852  rnoprab  5854  ov6g  5908  1st0  6042  2nd0  6043  dfmpo  6120  algrflem  6126  dftpos2  6158  tposoprab  6177  tposmpo  6178  tfrlem8  6215  frecsuc  6304  df2o3  6327  sbthlemi5  6849  sup00  6890  casedm  6971  djudm  6990  axi2m1  7690  2p2e4  8854  numsuc  9202  numsucc  9228  decmul10add  9257  5p5e10  9259  6p4e10  9260  7p3e10  9263  xnegmnf  9619  pnfaddmnf  9640  fz0tp  9908  fzo0to2pr  10002  fzo0to3tp  10003  fzo0to42pr  10004  0tonninf  10219  1tonninf  10220  inftonninf  10221  sq4e2t8  10397  i4  10402  fac1  10482  fac3  10485  abs0  10837  absi  10838  trirecip  11277  geoihalfsum  11298  esum  11375  tan0  11445  ef01bndlem  11470  3dvdsdec  11569  3dvds2dec  11570  3lcm2e6woprm  11774  6lcm4e12  11775  ennnfonelem1  11927  ndxarg  11992  setsfun  12004  setsfun0  12005  txbasval  12446  cnmpt1st  12467  cnmpt2nd  12468  dvmptidcn  12857  cos2pi  12898  tan4thpi  12935  sincos6thpi  12936  pwf1oexmid  13224  isomninnlem  13255
  Copyright terms: Public domain W3C validator