Theorem 3eqtr3rd 2276

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

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

This theorem is referenced by:  fcofo  5964  fcof1o  5969  frecabcl  6644  nnaword  6758  nninfisol  7438  enomnilem  7443  fodju0  7452  enmkvlem  7466  enwomnilem  7474  pn0sr  8103  negeu  8482  add20  8767  2halves  9488  lincmble  10360  bcnn  11148  bcpasc  11157  wrdeqs1cat  11441  resqrexlemover  11725  fsumneg  12167  geolim  12227  geolim2  12228  mertensabs  12253  sincossq  12464  demoivre  12489  eirraplem  12493  gcdid  12712  gcdmultipled  12719  phiprmpw  12949  pythagtriplem12  13003  expnprm  13081  ballotfilemrinv0  13225  imasbas  13576  imasplusg  13577  imasmulr  13578  grpinvid1  13812  grpnpcan  13852  grplactcnv  13862  ghmgrp  13876  conjghm  14034  ringnegl  14299  ringnegr  14300  ringmneg2  14302  ring1  14307  rdivmuldivd  14394  lmodfopne  14605  lmodvsneg  14610  ioo2bl  15547  ptolemy  15820  coskpi  15844  logbgcd1irr  15963  logbgcd1irraplemap  15965  lgseisenlem3  16076  lgseisenlem4  16077  lgsquadlem1  16081  lgsquadlem2  16082