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

Theorem 3eqtr3ri 2169
 Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)
Hypotheses
Ref Expression
3eqtr3i.1 𝐴 = 𝐵
3eqtr3i.2 𝐴 = 𝐶
3eqtr3i.3 𝐵 = 𝐷
Assertion
Ref Expression
3eqtr3ri 𝐷 = 𝐶

Proof of Theorem 3eqtr3ri
StepHypRef Expression
1 3eqtr3i.3 . 2 𝐵 = 𝐷
2 3eqtr3i.1 . . 3 𝐴 = 𝐵
3 3eqtr3i.2 . . 3 𝐴 = 𝐶
42, 3eqtr3i 2162 . 2 𝐵 = 𝐶
51, 4eqtr3i 2162 1 𝐷 = 𝐶
 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  8952  rei  10685  resqrexlemover  10796  cos1bnd  11479  6gcd4e2  11696  3lcm2e6  11851  cosq23lt0  12938  sincos4thpi  12945  sincos6thpi  12947  cosq34lt1  12955
 Copyright terms: Public domain W3C validator