Theorem 3eqtr2rd 2274

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr2rd	⊢ (𝜑 → 𝐷 = 𝐴)

Proof of Theorem 3eqtr2rd

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

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  difinfsn  7404  nnnninfeq  7432  prarloclemlo  7825  recexgt0sr  8104  xp1d2m1eqxm1d2  9508  qnegmod  10755  modqeqmodmin  10780  faclbnd2  11129  cats1un  11438  cjmulval  11598  fsumsplit  12118  fzosump1  12128  isumclim3  12134  bcxmas  12200  trireciplem  12211  geo2sum  12225  geo2lim  12227  geoisum1c  12231  cvgratnnlemseq  12237  mertenslemi1  12246  fprodsplitdc  12307  eftlub  12401  addsin  12453  subsin  12454  subcos  12458  qredeu  12819  nn0sqrtelqelz  12928  4sqlem15  13128  strslfv2d  13339  mulgaddcomlem  13898  conjghm  14029  dvexp  15702  tangtx  15829  logsqrt  15914  mpodvdsmulf1o  15984  lgsquad2lem1  16080  2sqlem8  16122