ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3eqtr3i Unicode 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  |-  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 2104 . 2  |-  B  =  C
4 3eqtr3i.3 . 2  |-  B  =  D
53, 4eqtr3i 2104 1  |-  C  =  D
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  3184  indif1  3216  difundir  3224  difindir  3226  dif32  3234  resmpt3  4687  xp0  4773  fvsnun1  5392  caov12  5720  caov13  5722  rec1nq  6647  halfnqq  6662  negsubdii  7460  halfpm6th  8318  decmul1  8621  i4  9674  fac4  9757  imi  9925  resqrexlemover  10034  znnen  10709  ex-bc  10717  ex-gcd  10719
  Copyright terms: Public domain W3C validator