Theorem 3eqtr2rd 2246

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  difinfsn  7217  nnnninfeq  7245  prarloclemlo  7627  recexgt0sr  7906  xp1d2m1eqxm1d2  9310  qnegmod  10536  modqeqmodmin  10561  faclbnd2  10909  cats1un  11197  cjmulval  11274  fsumsplit  11793  fzosump1  11803  isumclim3  11809  bcxmas  11875  trireciplem  11886  geo2sum  11900  geo2lim  11902  geoisum1c  11906  cvgratnnlemseq  11912  mertenslemi1  11921  fprodsplitdc  11982  eftlub  12076  addsin  12128  subsin  12129  subcos  12133  qredeu  12494  nn0sqrtelqelz  12603  4sqlem15  12803  strslfv2d  12950  mulgaddcomlem  13556  conjghm  13687  dvexp  15258  tangtx  15385  logsqrt  15470  mpodvdsmulf1o  15537  lgsquad2lem1  15633  2sqlem8  15675