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

Theorem 3eqtr3i 2166
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 2160 . 2  |-  B  =  C
4 3eqtr3i.3 . 2  |-  B  =  D
53, 4eqtr3i 2160 1  |-  C  =  D
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 2119
This theorem depends on definitions:  df-bi 116  df-cleq 2130
This theorem is referenced by:  csbvarg  3025  un12  3229  in12  3282  indif1  3316  difundir  3324  difindir  3326  dif32  3334  resmpt3  4863  xp0  4953  fvsnun1  5610  caov12  5952  caov13  5954  djuassen  7066  xpdjuen  7067  rec1nq  7196  halfnqq  7211  negsubdii  8040  halfpm6th  8933  decmul1  9238  i4  10388  fac4  10472  imi  10665  resqrexlemover  10775  ef01bndlem  11452  znnen  11900  sn0cld  12295  cospi  12870  sincos4thpi  12910  sincos3rdpi  12913  ex-bc  12930  ex-gcd  12932
  Copyright terms: Public domain W3C validator