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

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

Proof of Theorem 3eqtri
StepHypRef Expression
1 3eqtri.1 . 2 A = B
2 3eqtri.2 . . 3 B = 𝐶
3 3eqtri.3 . . 3 𝐶 = 𝐷
42, 3eqtri 2057 . 2 B = 𝐷
51, 4eqtri 2057 1 A = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  csbid  2853  un23  3096  in32  3143  dfrab2  3206  difun2  3296  tpidm23  3462  unisn  3587  dfiunv2  3684  uniop  3983  suc0  4114  unisuc  4116  iunsuc  4123  xpun  4344  dfrn2  4466  dfdmf  4471  dfrnf  4518  res0  4559  resres  4567  xpssres  4588  dfima2  4613  imai  4624  ima0  4627  imaundir  4680  xpima1  4710  xpima2m  4711  dmresv  4722  rescnvcnv  4726  dmtpop  4739  rnsnopg  4742  resdmres  4755  dmmpt  4759  dmco  4772  co01  4778  fpr  5288  fmptpr  5298  fvsnun2  5304  mpt20  5516  dmoprab  5527  rnoprab  5529  ov6g  5580  1st0  5713  2nd0  5714  dfmpt2  5786  algrflem  5792  dftpos2  5817  tposoprab  5836  tposmpt2  5837  tfrlem8  5875  df2o3  5953  axi2m1  6759  2p2e4  7815  numsuc  8155  numsucc  8169  xnegmnf  8512  fz0tp  8751  fzo0to2pr  8844  fzo0to3tp  8845  fzo0to42pr  8846  i4  9008  abs0  9222  absi  9223
  Copyright terms: Public domain W3C validator