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

Theorem 3eqtr4a 2198
 Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4a.1
3eqtr4a.2
3eqtr4a.3
Assertion
Ref Expression
3eqtr4a

Proof of Theorem 3eqtr4a
StepHypRef Expression
1 3eqtr4a.2 . . 3
2 3eqtr4a.1 . . 3
31, 2syl6eq 2188 . 2
4 3eqtr4a.3 . 2
53, 4eqtr4d 2175 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1331 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-cleq 2132 This theorem is referenced by:  uniintsnr  3807  fndmdifcom  5526  offres  6033  1stval2  6053  2ndval2  6054  ecovcom  6536  ecovass  6538  ecovdi  6540  zeo  9156  xnegneg  9616  xaddcom  9644  xaddid1  9645  xnegdi  9651  fzsuc2  9859  expnegap0  10301  facp1  10476  bcpasc  10512  hashfzp1  10570  resunimafz0  10574  absexp  10851  iooinsup  11046  fsumf1o  11159  fsumadd  11175  fisumrev2  11215  fsumparts  11239  efexp  11388  tanval2ap  11420  gcdcom  11662  gcd0id  11667  dfgcd3  11698  gcdass  11703  lcmcom  11745  lcmneg  11755  lcmass  11766  sqrt2irrlem  11839  nn0gcdsq  11878  dfphi2  11896  setscom  11999  restco  12343  txtopon  12431  dvef  12856
 Copyright terms: Public domain W3C validator