Theorem 3eqtr2rd 2217

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  difinfsn  7101  nnnninfeq  7128  prarloclemlo  7495  recexgt0sr  7774  xp1d2m1eqxm1d2  9173  qnegmod  10371  modqeqmodmin  10396  faclbnd2  10724  cjmulval  10899  fsumsplit  11417  fzosump1  11427  isumclim3  11433  bcxmas  11499  trireciplem  11510  geo2sum  11524  geo2lim  11526  geoisum1c  11530  cvgratnnlemseq  11536  mertenslemi1  11545  fprodsplitdc  11606  eftlub  11700  addsin  11752  subsin  11753  subcos  11757  qredeu  12099  nn0sqrtelqelz  12208  strslfv2d  12507  mulgaddcomlem  13011  dvexp  14260  tangtx  14344  logsqrt  14428  2sqlem8  14555