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

Theorem 3eqtr4ri 2149
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 2141 . 2 𝐷 = 𝐴
4 3eqtr4i.2 . 2 𝐶 = 𝐴
53, 4eqtr4i 2141 1 𝐷 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  cbvreucsf  3034  dfif6  3446  qdass  3590  tpidm12  3592  unipr  3720  dfdm4  4701  dmun  4716  resres  4801  inres  4806  resdifcom  4807  resiun1  4808  imainrect  4954  coundi  5010  coundir  5011  funopg  5127  offres  6001  mpomptsx  6063  cnvoprab  6099  snec  6458  halfpm6th  8908  numsucc  9189  decbin2  9290  fsumadd  11143  fsum2d  11172  znnen  11838
  Copyright terms: Public domain W3C validator