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

Theorem 3eqtr4a 2176
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 2166 . 2 (𝜑𝐶 = 𝐵)
4 3eqtr4a.3 . 2 (𝜑𝐷 = 𝐵)
53, 4eqtr4d 2153 1 (𝜑𝐶 = 𝐷)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316
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 1408  ax-gen 1410  ax-4 1472  ax-17 1491  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-cleq 2110
This theorem is referenced by:  uniintsnr  3777  fndmdifcom  5494  offres  6001  1stval2  6021  2ndval2  6022  ecovcom  6504  ecovass  6506  ecovdi  6508  zeo  9124  xnegneg  9584  xaddcom  9612  xaddid1  9613  xnegdi  9619  fzsuc2  9827  expnegap0  10269  facp1  10444  bcpasc  10480  hashfzp1  10538  resunimafz0  10542  absexp  10819  iooinsup  11014  fsumf1o  11127  fsumadd  11143  fisumrev2  11183  fsumparts  11207  efexp  11315  tanval2ap  11347  gcdcom  11589  gcd0id  11594  dfgcd3  11625  gcdass  11630  lcmcom  11672  lcmneg  11682  lcmass  11693  sqrt2irrlem  11766  nn0gcdsq  11805  dfphi2  11823  setscom  11926  restco  12270  txtopon  12358  dvef  12783
  Copyright terms: Public domain W3C validator