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

Theorem 3eqtr4a 2199
 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 2189 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4a.3 . 2 (𝜑𝐷 = 𝐵)
53, 4eqtr4d 2176 1 (𝜑𝐶 = 𝐷)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1332 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 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122 This theorem depends on definitions:  df-bi 116  df-cleq 2133 This theorem is referenced by:  uniintsnr  3814  fndmdifcom  5533  offres  6040  1stval2  6060  2ndval2  6061  ecovcom  6543  ecovass  6545  ecovdi  6547  zeo  9179  xnegneg  9645  xaddcom  9673  xaddid1  9674  xnegdi  9680  fzsuc2  9889  expnegap0  10331  facp1  10507  bcpasc  10543  hashfzp1  10601  resunimafz0  10605  absexp  10882  iooinsup  11077  fsumf1o  11190  fsumadd  11206  fisumrev2  11246  fsumparts  11270  efexp  11423  tanval2ap  11454  gcdcom  11696  gcd0id  11701  dfgcd3  11732  gcdass  11737  lcmcom  11779  lcmneg  11789  lcmass  11800  sqrt2irrlem  11873  nn0gcdsq  11912  dfphi2  11930  setscom  12036  restco  12380  txtopon  12468  dvef  12894
 Copyright terms: Public domain W3C validator