Theorem 3eqtr3rd 2280

Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)

Hypotheses

Ref	Expression
3eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
2		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtr3d 2273	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2273	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  fcofo  5984  fcof1o  5989  frecabcl  6664  nnaword  6778  nninfisol  7467  enomnilem  7472  fodju0  7481  enmkvlem  7495  enwomnilem  7503  pn0sr  8132  negeu  8511  add20  8796  2halves  9517  lincmble  10389  bcnn  11178  bcpasc  11187  wrdeqs1cat  11475  resqrexlemover  11759  fsumneg  12201  geolim  12261  geolim2  12262  mertensabs  12287  sincossq  12498  demoivre  12523  eirraplem  12527  gcdid  12746  gcdmultipled  12753  phiprmpw  12983  pythagtriplem12  13037  expnprm  13115  ballotfilemrinv0  13259  imasbas  13611  imasplusg  13612  imasmulr  13613  grpinvid1  13840  grpnpcan  13880  grplactcnv  13890  ghmgrp  13904  conjghm  14062  ringnegl  14339  ringnegr  14340  ringmneg2  14342  ring1  14347  rdivmuldivd  14434  lmodfopne  14646  lmodvsneg  14651  ioo2bl  15635  ptolemy  15908  coskpi  15932  logbgcd1irr  16052  logbgcd1irraplemap  16054  birthdaylem2  16071  lgseisenlem3  16174  lgseisenlem4  16175  lgsquadlem1  16179  lgsquadlem2  16180