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

Theorem 3eqtr3i 2168
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 2162 . 2 𝐵 = 𝐶
4 3eqtr3i.3 . 2 𝐵 = 𝐷
53, 4eqtr3i 2162 1 𝐶 = 𝐷
Colors of variables: wff set class
Syntax hints:   = wceq 1331
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132
This theorem is referenced by:  csbvarg  3030  un12  3234  in12  3287  indif1  3321  difundir  3329  difindir  3331  dif32  3339  resmpt3  4868  xp0  4958  fvsnun1  5617  caov12  5959  caov13  5961  djuassen  7080  xpdjuen  7081  rec1nq  7217  halfnqq  7232  negsubdii  8061  halfpm6th  8954  decmul1  9259  i4  10409  fac4  10493  imi  10686  resqrexlemover  10796  ef01bndlem  11476  znnen  11924  sn0cld  12322  cospi  12905  sincos4thpi  12945  sincos3rdpi  12948  ex-bc  13048  ex-gcd  13050
  Copyright terms: Public domain W3C validator