Theorem 3eqtr2rd 2236

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 2232	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2230	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  difinfsn  7175  nnnninfeq  7203  prarloclemlo  7578  recexgt0sr  7857  xp1d2m1eqxm1d2  9261  qnegmod  10478  modqeqmodmin  10503  faclbnd2  10851  cjmulval  11070  fsumsplit  11589  fzosump1  11599  isumclim3  11605  bcxmas  11671  trireciplem  11682  geo2sum  11696  geo2lim  11698  geoisum1c  11702  cvgratnnlemseq  11708  mertenslemi1  11717  fprodsplitdc  11778  eftlub  11872  addsin  11924  subsin  11925  subcos  11929  qredeu  12290  nn0sqrtelqelz  12399  4sqlem15  12599  strslfv2d  12746  mulgaddcomlem  13351  conjghm  13482  dvexp  15031  tangtx  15158  logsqrt  15243  mpodvdsmulf1o  15310  lgsquad2lem1  15406  2sqlem8  15448