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

Theorem 3eqtr3i 2146
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 2140 . 2  |-  B  =  C
4 3eqtr3i.3 . 2  |-  B  =  D
53, 4eqtr3i 2140 1  |-  C  =  D
Colors of variables: wff set class
Syntax hints:    = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  csbvarg  3000  un12  3204  in12  3257  indif1  3291  difundir  3299  difindir  3301  dif32  3309  resmpt3  4838  xp0  4928  fvsnun1  5585  caov12  5927  caov13  5929  djuassen  7041  xpdjuen  7042  rec1nq  7171  halfnqq  7186  negsubdii  8015  halfpm6th  8908  decmul1  9213  i4  10363  fac4  10447  imi  10640  resqrexlemover  10750  ef01bndlem  11390  znnen  11838  sn0cld  12233  cospi  12808  sincos4thpi  12848  sincos3rdpi  12851  ex-bc  12868  ex-gcd  12870
  Copyright terms: Public domain W3C validator