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

Theorem 3eqtr3ri 2169
Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
Hypotheses
Ref Expression
3eqtr3i.1  |-  A  =  B
3eqtr3i.2  |-  A  =  C
3eqtr3i.3  |-  B  =  D
Assertion
Ref Expression
3eqtr3ri  |-  D  =  C

Proof of Theorem 3eqtr3ri
StepHypRef Expression
1 3eqtr3i.3 . 2  |-  B  =  D
2 3eqtr3i.1 . . 3  |-  A  =  B
3 3eqtr3i.2 . . 3  |-  A  =  C
42, 3eqtr3i 2162 . 2  |-  B  =  C
51, 4eqtr3i 2162 1  |-  D  =  C
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:  indif2  3320  resdm2  5029  co01  5053  cocnvres  5063  undifdc  6812  1mhlfehlf  8950  rei  10683  resqrexlemover  10794  cos1bnd  11477  6gcd4e2  11694  3lcm2e6  11849  cosq23lt0  12936  sincos4thpi  12943  sincos6thpi  12945  cosq34lt1  12953
  Copyright terms: Public domain W3C validator