Theorem 3eqtr3rd 2274

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 2267	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2267	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2214

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

This theorem is referenced by:  fcofo  5956  fcof1o  5961  frecabcl  6629  nnaword  6743  nninfisol  7423  enomnilem  7428  fodju0  7437  enmkvlem  7451  enwomnilem  7459  pn0sr  8085  negeu  8463  add20  8747  2halves  9466  lincmble  10336  bcnn  11118  bcpasc  11127  wrdeqs1cat  11408  resqrexlemover  11691  fsumneg  12133  geolim  12193  geolim2  12194  mertensabs  12219  sincossq  12430  demoivre  12455  eirraplem  12459  gcdid  12678  gcdmultipled  12685  phiprmpw  12915  pythagtriplem12  12969  expnprm  13047  imasbas  13512  imasplusg  13513  imasmulr  13514  grpinvid1  13757  grpnpcan  13797  grplactcnv  13807  ghmgrp  13827  conjghm  13985  ringnegl  14187  ringnegr  14188  ringmneg2  14190  ring1  14195  rdivmuldivd  14281  lmodfopne  14466  lmodvsneg  14471  ioo2bl  15408  ptolemy  15681  coskpi  15705  logbgcd1irr  15824  logbgcd1irraplemap  15826  lgseisenlem3  15937  lgseisenlem4  15938  lgsquadlem1  15942  lgsquadlem2  15943