Theorem 3eqtr4a 2288

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 2278	. 2 ⊢ (𝜑 → 𝐶 = 𝐵)
4		3eqtr4a.3	. 2 ⊢ (𝜑 → 𝐷 = 𝐵)
5	3, 4	eqtr4d 2265	1 ⊢ (𝜑 → 𝐶 = 𝐷)

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  uniintsnr  3958  fndmdifcom  5740  funopsn  5816  offres  6278  1stval2  6299  2ndval2  6300  ecovcom  6787  ecovass  6789  ecovdi  6791  nnnninfeq2  7292  zeo  9548  xnegneg  10025  xaddcom  10053  xaddid1  10054  xnegdi  10060  fzsuc2  10271  expnegap0  10764  facp1  10947  bcpasc  10983  hashfzp1  11041  resunimafz0  11048  ccat1st1st  11167  absexp  11585  iooinsup  11783  fsumf1o  11896  fsumadd  11912  fisumrev2  11952  fsumparts  11976  fprodf1o  12094  fprodmul  12097  efexp  12188  tanval2ap  12219  gcdcom  12489  gcd0id  12495  dfgcd3  12526  gcdass  12531  lcmcom  12581  lcmneg  12591  lcmass  12602  sqrt2irrlem  12678  nn0gcdsq  12717  dfphi2  12737  eulerthlemth  12749  pcneg  12843  setscom  13067  gsumfzfsumlem0  14544  restco  14842  txtopon  14930  dvmptid  15384  dvef  15395  fsumdvdsmul  15659  lgsneg  15697  lgsneg1  15698  lgsdir2  15706  lgsdir  15708  lgsdi  15710  lgsquad2lem2  15755