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  5963  fcof1o  5968  frecabcl  6643  nnaword  6757  nninfisol  7437  enomnilem  7442  fodju0  7451  enmkvlem  7465  enwomnilem  7473  pn0sr  8102  negeu  8481  add20  8766  2halves  9487  lincmble  10359  bcnn  11147  bcpasc  11156  wrdeqs1cat  11440  resqrexlemover  11724  fsumneg  12166  geolim  12226  geolim2  12227  mertensabs  12252  sincossq  12463  demoivre  12488  eirraplem  12492  gcdid  12711  gcdmultipled  12718  phiprmpw  12948  pythagtriplem12  13002  expnprm  13080  ballotfilemrinv0  13224  imasbas  13575  imasplusg  13576  imasmulr  13577  grpinvid1  13811  grpnpcan  13851  grplactcnv  13861  ghmgrp  13875  conjghm  14033  ringnegl  14298  ringnegr  14299  ringmneg2  14301  ring1  14306  rdivmuldivd  14393  lmodfopne  14604  lmodvsneg  14609  ioo2bl  15546  ptolemy  15819  coskpi  15843  logbgcd1irr  15962  logbgcd1irraplemap  15964  lgseisenlem3  16075  lgseisenlem4  16076  lgsquadlem1  16080  lgsquadlem2  16081