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

Theorem 3eqtr4ri 2221
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 2213 . 2 𝐷 = 𝐴
4 3eqtr4i.2 . 2 𝐶 = 𝐴
53, 4eqtr4i 2213 1 𝐷 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2171
This theorem depends on definitions:  df-bi 117  df-cleq 2182
This theorem is referenced by:  cbvreucsf  3136  dfif6  3551  qdass  3704  tpidm12  3706  unipr  3838  dfdm4  4837  dmun  4852  resres  4937  inres  4942  resdifcom  4943  resiun1  4944  imainrect  5092  coundi  5148  coundir  5149  funopg  5269  offres  6160  mpomptsx  6222  cnvoprab  6259  snec  6622  halfpm6th  9169  numsucc  9453  decbin2  9554  fsumadd  11446  fsum2d  11475  fprodmul  11631  fprodfac  11655  fprodrec  11669  znnen  12449
  Copyright terms: Public domain W3C validator