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  8480  add20  8765  2halves  9484  lincmble  10356  bcnn  11144  bcpasc  11153  wrdeqs1cat  11437  resqrexlemover  11720  fsumneg  12162  geolim  12222  geolim2  12223  mertensabs  12248  sincossq  12459  demoivre  12484  eirraplem  12488  gcdid  12707  gcdmultipled  12714  phiprmpw  12944  pythagtriplem12  12998  expnprm  13076  ballotfilemrinv0  13220  imasbas  13604  imasplusg  13605  imasmulr  13606  grpinvid1  13849  grpnpcan  13889  grplactcnv  13899  ghmgrp  13919  conjghm  14077  ringnegl  14279  ringnegr  14280  ringmneg2  14282  ring1  14287  rdivmuldivd  14374  lmodfopne  14586  lmodvsneg  14591  ioo2bl  15528  ptolemy  15801  coskpi  15825  logbgcd1irr  15944  logbgcd1irraplemap  15946  lgseisenlem3  16057  lgseisenlem4  16058  lgsquadlem1  16062  lgsquadlem2  16063