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

Theorem 3eqtr3ri 2200
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 2193 . 2 𝐵 = 𝐶
51, 4eqtr3i 2193 1 𝐷 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1348
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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152
This theorem depends on definitions:  df-bi 116  df-cleq 2163
This theorem is referenced by:  indif2  3371  resdm2  5099  co01  5123  cocnvres  5133  undifdc  6897  1mhlfehlf  9083  rei  10850  resqrexlemover  10961  cos1bnd  11709  6gcd4e2  11937  3lcm2e6  12101  cosq23lt0  13469  sincos4thpi  13476  sincos6thpi  13478  cosq34lt1  13486
  Copyright terms: Public domain W3C validator