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

Theorem 3eqtri 2046
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 2042 . 2 B = 𝐷
51, 4eqtri 2042 1 A = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1228
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 1316  ax-gen 1318  ax-4 1381  ax-17 1400  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-cleq 2015
This theorem is referenced by:  csbid  2836  un23  3079  in32  3126  dfrab2  3189  difun2  3279  tpidm23  3445  unisn  3570  dfiunv2  3667  uniop  3966  suc0  4097  unisuc  4099  iunsuc  4106  xpun  4328  dfrn2  4450  dfdmf  4455  dfrnf  4502  res0  4543  resres  4551  xpssres  4572  dfima2  4597  imai  4608  ima0  4611  imaundir  4664  xpima1  4694  xpima2m  4695  dmresv  4706  rescnvcnv  4710  dmtpop  4723  rnsnopg  4726  resdmres  4739  dmmpt  4743  dmco  4756  co01  4762  fpr  5270  fmptpr  5280  fvsnun2  5286  mpt20  5497  dmoprab  5508  rnoprab  5510  ov6g  5561  1st0  5694  2nd0  5695  dfmpt2  5767  algrflem  5773  dftpos2  5798  tposoprab  5817  tposmpt2  5818  tfrlem8  5856  df2o3  5929  axi2m1  6569
  Copyright terms: Public domain W3C validator