Theorem 3eqtr4a 2297

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

Step	Hyp	Ref	Expression
1		3eqtr4a.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eqtr4a.1	. . 3 ⊢ 𝐴 = 𝐵
3	1, 2	eqtrdi 2287	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2274	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-cleq 2231

This theorem is referenced by:  uniintsnr  4001  fndmdifcom  5806  funopsn  5882  offres  6358  1stval2  6379  2ndval2  6380  ecovcom  6906  ecovass  6908  ecovdi  6910  nnnninfeq2  7459  zeo  9730  xnegneg  10214  xaddcom  10242  xaddid1  10243  xnegdi  10249  fzsuc2  10464  expnegap0  10962  resq01  11073  facp1  11146  bcpasc  11182  hashfzp1  11243  resunimafz0  11252  hashfibclem  11260  hashfibc  11261  hashf1  11265  ccat1st1st  11387  sq01  11638  absexp  11823  iooinsup  12021  fsumf1o  12135  fsumadd  12151  fisumrev2  12191  fsumparts  12215  fprodf1o  12333  fprodmul  12336  efexp  12427  tanval2ap  12458  gcdcom  12728  gcd0id  12734  dfgcd3  12765  gcdass  12770  lcmcom  12820  lcmneg  12830  lcmass  12841  sqrt2irrlem  12917  nn0gcdsq  12956  dfphi2  12976  eulerthlemth  12988  pcneg  13082  setscom  13370  restco  15198  txtopon  15286  dvmptid  15740  dvef  15751  logfac  15918  fsumdvdsmul  16019  lgsneg  16057  lgsneg1  16058  lgsdir2  16066  lgsdir  16068  lgsdi  16070  lgsquad2lem2  16115  egrsubgr  16418