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

Theorem 3eqtr4ri 2087
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  |-  A  =  B
3eqtr4i.2  |-  C  =  A
3eqtr4i.3  |-  D  =  B
Assertion
Ref Expression
3eqtr4ri  |-  D  =  C

Proof of Theorem 3eqtr4ri
StepHypRef Expression
1 3eqtr4i.3 . . 3  |-  D  =  B
2 3eqtr4i.1 . . 3  |-  A  =  B
31, 2eqtr4i 2079 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2079 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1259
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-cleq 2049
This theorem is referenced by:  cbvreucsf  2938  dfif6  3361  qdass  3495  tpidm12  3497  unipr  3622  dfdm4  4555  dmun  4570  resres  4652  inres  4657  resiun1  4658  imainrect  4794  coundi  4850  coundir  4851  funopg  4962  offres  5790  mpt2mptsx  5851  cnvoprab  5883  snec  6198  halfpm6th  8202  numsucc  8466  decbin2  8567
  Copyright terms: Public domain W3C validator