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
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  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