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

Theorem 3eqtr4ri 2068
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 A = B
3eqtr4i.2 𝐶 = A
3eqtr4i.3 𝐷 = B
Assertion
Ref Expression
3eqtr4ri 𝐷 = 𝐶

Proof of Theorem 3eqtr4ri
StepHypRef Expression
1 3eqtr4i.3 . . 3 𝐷 = B
2 3eqtr4i.1 . . 3 A = B
31, 2eqtr4i 2060 . 2 𝐷 = A
4 3eqtr4i.2 . 2 𝐶 = A
53, 4eqtr4i 2060 1 𝐷 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1242
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-cleq 2030
This theorem is referenced by:  cbvreucsf  2904  dfif6  3327  qdass  3458  tpidm12  3460  unipr  3585  dfdm4  4470  dmun  4485  resres  4567  inres  4572  resiun1  4573  imainrect  4709  coundi  4765  coundir  4766  funopg  4877  offres  5704  mpt2mptsx  5765  snec  6103  halfpm6th  7882  numsucc  8129  decbin2  8207
  Copyright terms: Public domain W3C validator