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

Theorem 3eqtr4ri 2209
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 2201 . 2 𝐷 = 𝐴
4 3eqtr4i.2 . 2 𝐶 = 𝐴
53, 4eqtr4i 2201 1 𝐷 = 𝐶
Colors of variables: wff set class
Syntax hints:   = wceq 1353
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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-cleq 2170
This theorem is referenced by:  cbvreucsf  3123  dfif6  3538  qdass  3691  tpidm12  3693  unipr  3825  dfdm4  4821  dmun  4836  resres  4921  inres  4926  resdifcom  4927  resiun1  4928  imainrect  5076  coundi  5132  coundir  5133  funopg  5252  offres  6138  mpomptsx  6200  cnvoprab  6237  snec  6598  halfpm6th  9141  numsucc  9425  decbin2  9526  fsumadd  11416  fsum2d  11445  fprodmul  11601  fprodfac  11625  fprodrec  11639  znnen  12401
  Copyright terms: Public domain W3C validator