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

Theorem 3eqtr3i 2110
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 𝐴 = 𝐵
3eqtr3i.2 𝐴 = 𝐶
3eqtr3i.3 𝐵 = 𝐷
Assertion
Ref Expression
3eqtr3i 𝐶 = 𝐷

Proof of Theorem 3eqtr3i
StepHypRef Expression
1 3eqtr3i.1 . . 3 𝐴 = 𝐵
2 3eqtr3i.2 . . 3 𝐴 = 𝐶
31, 2eqtr3i 2104 . 2 𝐵 = 𝐶
4 3eqtr3i.3 . 2 𝐵 = 𝐷
53, 4eqtr3i 2104 1 𝐶 = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1285
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-cleq 2075
This theorem is referenced by:  csbvarg  2934  un12  3131  in12  3178  indif1  3210  difundir  3218  difindir  3220  dif32  3228  resmpt3  4681  xp0  4767  fvsnun1  5386  caov12  5714  caov13  5716  rec1nq  6636  halfnqq  6651  negsubdii  7449  halfpm6th  8307  decmul1  8610  i4  9663  fac4  9746  imi  9914  resqrexlemover  10023  ex-bc  10702  ex-gcd  10704
  Copyright terms: Public domain W3C validator