Theorem 3eqtr2rd 2233

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 2229	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2227	1 ⊢ (𝜑 → 𝐷 = 𝐴)

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  difinfsn  7161  nnnninfeq  7189  prarloclemlo  7556  recexgt0sr  7835  xp1d2m1eqxm1d2  9238  qnegmod  10443  modqeqmodmin  10468  faclbnd2  10816  cjmulval  11035  fsumsplit  11553  fzosump1  11563  isumclim3  11569  bcxmas  11635  trireciplem  11646  geo2sum  11660  geo2lim  11662  geoisum1c  11666  cvgratnnlemseq  11672  mertenslemi1  11681  fprodsplitdc  11742  eftlub  11836  addsin  11888  subsin  11889  subcos  11893  qredeu  12238  nn0sqrtelqelz  12347  4sqlem15  12546  strslfv2d  12664  mulgaddcomlem  13218  conjghm  13349  dvexp  14890  tangtx  15014  logsqrt  15098  lgsquad2lem1  15238  2sqlem8  15280