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

Theorem 3eqtr4ri 2119
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 2111 . 2 𝐷 = 𝐴
4 3eqtr4i.2 . 2 𝐶 = 𝐴
53, 4eqtr4i 2111 1 𝐷 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1289
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 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070
This theorem depends on definitions:  df-bi 115  df-cleq 2081
This theorem is referenced by:  cbvreucsf  2992  dfif6  3395  qdass  3539  tpidm12  3541  unipr  3667  dfdm4  4628  dmun  4643  resres  4725  inres  4730  resdifcom  4731  resiun1  4732  imainrect  4876  coundi  4932  coundir  4933  funopg  5048  offres  5906  mpt2mptsx  5967  cnvoprab  5999  snec  6351  halfpm6th  8634  numsucc  8914  decbin2  9015  fsumadd  10796  fsum2d  10825  znnen  11485
  Copyright terms: Public domain W3C validator