Theorem 3eqtr4a 2290

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

Syntax hints:   → wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  uniintsnr  3964  fndmdifcom  5753  funopsn  5830  offres  6297  1stval2  6318  2ndval2  6319  ecovcom  6811  ecovass  6813  ecovdi  6815  nnnninfeq2  7328  zeo  9585  xnegneg  10068  xaddcom  10096  xaddid1  10097  xnegdi  10103  fzsuc2  10314  expnegap0  10810  facp1  10993  bcpasc  11029  hashfzp1  11089  resunimafz0  11096  ccat1st1st  11222  absexp  11657  iooinsup  11855  fsumf1o  11969  fsumadd  11985  fisumrev2  12025  fsumparts  12049  fprodf1o  12167  fprodmul  12170  efexp  12261  tanval2ap  12292  gcdcom  12562  gcd0id  12568  dfgcd3  12599  gcdass  12604  lcmcom  12654  lcmneg  12664  lcmass  12675  sqrt2irrlem  12751  nn0gcdsq  12790  dfphi2  12810  eulerthlemth  12822  pcneg  12916  setscom  13140  gsumfzfsumlem0  14619  restco  14917  txtopon  15005  dvmptid  15459  dvef  15470  fsumdvdsmul  15734  lgsneg  15772  lgsneg1  15773  lgsdir2  15781  lgsdir  15783  lgsdi  15785  lgsquad2lem2  15830  egrsubgr  16133