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

Theorem 3eqtr3i 2065
Description: An inference from three chained equalities. (Contributed by NM, 6-May-1994.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr3i.1 A = B
3eqtr3i.2 A = 𝐶
3eqtr3i.3 B = 𝐷
Assertion
Ref Expression
3eqtr3i 𝐶 = 𝐷

Proof of Theorem 3eqtr3i
StepHypRef Expression
1 3eqtr3i.1 . . 3 A = B
2 3eqtr3i.2 . . 3 A = 𝐶
31, 2eqtr3i 2059 . 2 B = 𝐶
4 3eqtr3i.3 . 2 B = 𝐷
53, 4eqtr3i 2059 1 𝐶 = 𝐷
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:  csbvarg  2871  un12  3095  in12  3142  indif1  3176  difundir  3184  difindir  3186  dif32  3194  resmpt3  4600  xp0  4686  fvsnun1  5303  caov12  5631  caov13  5633  rec1nq  6379  halfnqq  6393  negsubdii  7092  halfpm6th  7922  i4  9008  imi  9128
  Copyright terms: Public domain W3C validator