New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  3eqtri GIF version

Theorem 3eqtri 2377
 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 2373 . 2 B = D
51, 4eqtri 2373 1 A = D
 Colors of variables: wff setvar class Syntax hints:   = wceq 1642 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-11 1746  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-ex 1542  df-cleq 2346 This theorem is referenced by:  csbid  3143  un23  3422  in32  3467  dfrab2  3530  undifv  3624  undif2  3626  undifabs  3627  difun2  3629  difdifdir  3637  dfif4  3673  tpidm23  3823  unisn  3907  incompl  4073  pw10  4161  xpun  4834  dfdmf  4905  dfrnf  4962  res0  4977  resres  4980  resopab  4999  imai  5010  ima0  5013  epini  5021  imaundir  5040  dmtpop  5071  resdmres  5078  dmco  5089  coi2  5095  fvsnun1  5447  fvsnun2  5448  dmoprab  5574  rnoprab  5576  ov6g  5600  dmmpt  5683  rnmpt2  5717  cnvpprod  5841  mucid1  6143  sbthlem1  6203  scancan  6331
 Copyright terms: Public domain W3C validator