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

Theorem 3eqtr4ri 2068
 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 2060 . 2
4 3eqtr4i.2 . 2
53, 4eqtr4i 2060 1
 Colors of variables: wff set class Syntax hints:   wceq 1242 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1333  ax-gen 1335  ax-4 1397  ax-17 1416  ax-ext 2019 This theorem depends on definitions:  df-bi 110  df-cleq 2030 This theorem is referenced by:  cbvreucsf  2904  dfif6  3327  qdass  3458  tpidm12  3460  unipr  3585  dfdm4  4470  dmun  4485  resres  4567  inres  4572  resiun1  4573  imainrect  4709  coundi  4765  coundir  4766  funopg  4877  offres  5704  mpt2mptsx  5765  snec  6103  halfpm6th  7902  numsucc  8149  decbin2  8227
 Copyright terms: Public domain W3C validator