Theorem 3eqtr4rd 2138

Description: A deduction from three chained equalities. (Contributed by NM, 21-Sep-1995.)

Hypotheses

Ref	Expression
3eqtr4d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr4d.2	⊢ (𝜑 → 𝐶 = 𝐴)
3eqtr4d.3	⊢ (𝜑 → 𝐷 = 𝐵)

Assertion

Ref	Expression
3eqtr4rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr4rd

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

Syntax hints:   → wi 4   = wceq 1296

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-4 1452  ax-17 1471  ax-ext 2077

This theorem depends on definitions:  df-bi 116  df-cleq 2088

This theorem is referenced by:  csbcnvg  4651  fvco4  5411  phplem4  6651  phplem4on  6663  recexnq  7046  prarloclemcalc  7158  addcomprg  7234  mulcomprg  7236  mulcmpblnrlemg  7383  axmulass  7505  divnegap  8270  modqlt  9889  modqmulnn  9898  iseqvalt  10019  seq3val  10020  seq3caopr3  10047  seq3f1olemqsumkj  10064  seq3f1olemqsumk  10065  seq3f1olemqsum  10066  seq3f1o  10070  bcval5  10302  omgadd  10341  seq3coll  10378  cjreb  10431  recj  10432  imcj  10440  imval2  10459  resqrexlemover  10574  sqrtmul  10599  amgm2  10682  maxabslemab  10770  xrmaxadd  10820  summodclem2a  10940  fsumf1o  10949  sumsnf  10968  sumsplitdc  10991  fsummulc2  11007  binom  11043  bcxmas  11048  expcnvap0  11061  expcnv  11063  cvgratnnlemnexp  11083  cvgratnnlemmn  11084  ege2le3  11126  efaddlem  11129  eftlub  11145  tanval3ap  11170  tannegap  11184  cosmul  11201  cos01bnd  11214  demoivreALT  11228  flodddiv4  11377  dfgcd3  11442  absmulgcd  11449  sqpweven  11596  2sqpwodd  11597  crth  11643  setsslnid  11710