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

Theorem 3eqtr4ri 2116
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 2108 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2108 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1287
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 1379  ax-gen 1381  ax-4 1443  ax-17 1462  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-cleq 2078
This theorem is referenced by:  cbvreucsf  2981  dfif6  3381  qdass  3522  tpidm12  3524  unipr  3650  dfdm4  4596  dmun  4611  resres  4693  inres  4698  resiun1  4699  imainrect  4842  coundi  4898  coundir  4899  funopg  5013  offres  5863  mpt2mptsx  5924  cnvoprab  5956  snec  6305  halfpm6th  8569  numsucc  8848  decbin2  8949  znnen  11093
  Copyright terms: Public domain W3C validator