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  7580  recexgt0sr  7859  xp1d2m1eqxm1d2  9263  qnegmod  10480  modqeqmodmin  10505  faclbnd2  10853  cjmulval  11072  fsumsplit  11591  fzosump1  11601  isumclim3  11607  bcxmas  11673  trireciplem  11684  geo2sum  11698  geo2lim  11700  geoisum1c  11704  cvgratnnlemseq  11710  mertenslemi1  11719  fprodsplitdc  11780  eftlub  11874  addsin  11926  subsin  11927  subcos  11931  qredeu  12292  nn0sqrtelqelz  12401  4sqlem15  12601  strslfv2d  12748  mulgaddcomlem  13353  conjghm  13484  dvexp  15055  tangtx  15182  logsqrt  15267  mpodvdsmulf1o  15334  lgsquad2lem1  15430  2sqlem8  15472