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

Theorem 3eqtr4a 2236
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, 2eqtrdi 2226 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4a.3 . 2 (𝜑𝐷 = 𝐵)
53, 4eqtr4d 2213 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = 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:  uniintsnr  3878  fndmdifcom  5617  offres  6129  1stval2  6149  2ndval2  6150  ecovcom  6635  ecovass  6637  ecovdi  6639  nnnninfeq2  7120  zeo  9334  xnegneg  9807  xaddcom  9835  xaddid1  9836  xnegdi  9842  fzsuc2  10052  expnegap0  10501  facp1  10681  bcpasc  10717  hashfzp1  10775  resunimafz0  10782  absexp  11059  iooinsup  11256  fsumf1o  11369  fsumadd  11385  fisumrev2  11425  fsumparts  11449  fprodf1o  11567  fprodmul  11570  efexp  11661  tanval2ap  11692  gcdcom  11944  gcd0id  11950  dfgcd3  11981  gcdass  11986  lcmcom  12034  lcmneg  12044  lcmass  12055  sqrt2irrlem  12131  nn0gcdsq  12170  dfphi2  12190  eulerthlemth  12202  pcneg  12294  setscom  12472  restco  13307  txtopon  13395  dvef  13821  lgsneg  14058  lgsneg1  14059  lgsdir2  14067  lgsdir  14069  lgsdi  14071
  Copyright terms: Public domain W3C validator