Theorem 3eqtr4a 2265

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  uniintsnr  3927  fndmdifcom  5699  funopsn  5775  offres  6233  1stval2  6254  2ndval2  6255  ecovcom  6742  ecovass  6744  ecovdi  6746  nnnninfeq2  7246  zeo  9498  xnegneg  9975  xaddcom  10003  xaddid1  10004  xnegdi  10010  fzsuc2  10221  expnegap0  10714  facp1  10897  bcpasc  10933  hashfzp1  10991  resunimafz0  10998  ccat1st1st  11116  absexp  11465  iooinsup  11663  fsumf1o  11776  fsumadd  11792  fisumrev2  11832  fsumparts  11856  fprodf1o  11974  fprodmul  11977  efexp  12068  tanval2ap  12099  gcdcom  12369  gcd0id  12375  dfgcd3  12406  gcdass  12411  lcmcom  12461  lcmneg  12471  lcmass  12482  sqrt2irrlem  12558  nn0gcdsq  12597  dfphi2  12617  eulerthlemth  12629  pcneg  12723  setscom  12947  gsumfzfsumlem0  14423  restco  14721  txtopon  14809  dvmptid  15263  dvef  15274  fsumdvdsmul  15538  lgsneg  15576  lgsneg1  15577  lgsdir2  15585  lgsdir  15587  lgsdi  15589  lgsquad2lem2  15634