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

Theorem 3eqtr3i 2068
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  =  C
3eqtr3i.3  |-  B  =  D
Assertion
Ref Expression
3eqtr3i  |-  C  =  D

Proof of Theorem 3eqtr3i
StepHypRef Expression
1 3eqtr3i.1 . . 3  |-  A  =  B
2 3eqtr3i.2 . . 3  |-  A  =  C
31, 2eqtr3i 2062 . 2  |-  B  =  C
4 3eqtr3i.3 . 2  |-  B  =  D
53, 4eqtr3i 2062 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1243
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 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-cleq 2033
This theorem is referenced by:  csbvarg  2877  un12  3101  in12  3148  indif1  3182  difundir  3190  difindir  3192  dif32  3200  resmpt3  4657  xp0  4743  fvsnun1  5360  caov12  5689  caov13  5691  rec1nq  6493  halfnqq  6508  negsubdii  7296  halfpm6th  8145  i4  9355  imi  9500  resqrexlemover  9608
  Copyright terms: Public domain W3C validator