ILE Home 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