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

Theorem 3eqtr4ri 2071
 Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4i.1 𝐴 = 𝐵
3eqtr4i.2 𝐶 = 𝐴
3eqtr4i.3 𝐷 = 𝐵
Assertion
Ref Expression
3eqtr4ri 𝐷 = 𝐶

Proof of Theorem 3eqtr4ri
StepHypRef Expression
1 3eqtr4i.3 . . 3 𝐷 = 𝐵
2 3eqtr4i.1 . . 3 𝐴 = 𝐵
31, 2eqtr4i 2063 . 2 𝐷 = 𝐴
4 3eqtr4i.2 . 2 𝐶 = 𝐴
53, 4eqtr4i 2063 1 𝐷 = 𝐶
 Colors of variables: wff set class Syntax hints:   = wceq 1243 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-cleq 2033 This theorem is referenced by:  cbvreucsf  2910  dfif6  3333  qdass  3467  tpidm12  3469  unipr  3594  dfdm4  4527  dmun  4542  resres  4624  inres  4629  resiun1  4630  imainrect  4766  coundi  4822  coundir  4823  funopg  4934  offres  5762  mpt2mptsx  5823  snec  6167  halfpm6th  8145  numsucc  8393  decbin2  8471
 Copyright terms: Public domain W3C validator