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  3121  dfif6  3536  qdass  3689  tpidm12  3691  unipr  3823  dfdm4  4819  dmun  4834  resres  4919  inres  4924  resdifcom  4925  resiun1  4926  imainrect  5074  coundi  5130  coundir  5131  funopg  5250  offres  6135  mpomptsx  6197  cnvoprab  6234  snec  6595  halfpm6th  9138  numsucc  9422  decbin2  9523  fsumadd  11413  fsum2d  11442  fprodmul  11598  fprodfac  11622  fprodrec  11636  znnen  12398
  Copyright terms: Public domain W3C validator