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

Theorem 3eqtr4ri 2114
 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 2106 . 2 𝐷 = 𝐴
4 3eqtr4i.2 . 2 𝐶 = 𝐴
53, 4eqtr4i 2106 1 𝐷 = 𝐶
 Colors of variables: wff set class Syntax hints:   = wceq 1285 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065 This theorem depends on definitions:  df-bi 115  df-cleq 2076 This theorem is referenced by:  cbvreucsf  2976  dfif6  3371  qdass  3508  tpidm12  3510  unipr  3636  dfdm4  4576  dmun  4591  resres  4673  inres  4678  resiun1  4679  imainrect  4817  coundi  4873  coundir  4874  funopg  4985  offres  5815  mpt2mptsx  5876  cnvoprab  5908  snec  6256  halfpm6th  8395  numsucc  8674  decbin2  8775  znnen  10843
 Copyright terms: Public domain W3C validator