Theorem 3eqtr3rd 2235

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 2228	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2228	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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  fcofo  5828  fcof1o  5833  frecabcl  6454  nnaword  6566  nninfisol  7194  enomnilem  7199  fodju0  7208  enmkvlem  7222  enwomnilem  7230  pn0sr  7833  negeu  8212  add20  8495  2halves  9214  bcnn  10831  bcpasc  10840  resqrexlemover  11157  fsumneg  11597  geolim  11657  geolim2  11658  mertensabs  11683  sincossq  11894  demoivre  11919  eirraplem  11923  gcdid  12126  gcdmultipled  12133  phiprmpw  12363  pythagtriplem12  12416  expnprm  12494  imasbas  12893  imasplusg  12894  imasmulr  12895  grpinvid1  13127  grpnpcan  13167  grplactcnv  13177  ghmgrp  13191  conjghm  13349  ringnegl  13550  ringnegr  13551  ringmneg2  13553  ring1  13558  rdivmuldivd  13643  lmodfopne  13825  lmodvsneg  13830  ioo2bl  14730  ptolemy  15000  coskpi  15024  logbgcd1irr  15140  logbgcd1irraplemap  15142  lgseisenlem3  15229  lgseisenlem4  15230  lgsquadlem1  15234  lgsquadlem2  15235