Theorem 3eqtr3rd 2273

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

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

This theorem is referenced by:  fcofo  5935  fcof1o  5940  frecabcl  6608  nnaword  6722  nninfisol  7375  enomnilem  7380  fodju0  7389  enmkvlem  7403  enwomnilem  7411  pn0sr  8034  negeu  8413  add20  8697  2halves  9416  bcnn  11063  bcpasc  11072  wrdeqs1cat  11348  resqrexlemover  11631  fsumneg  12073  geolim  12133  geolim2  12134  mertensabs  12159  sincossq  12370  demoivre  12395  eirraplem  12399  gcdid  12618  gcdmultipled  12625  phiprmpw  12855  pythagtriplem12  12909  expnprm  12987  imasbas  13451  imasplusg  13452  imasmulr  13453  grpinvid1  13696  grpnpcan  13736  grplactcnv  13746  ghmgrp  13766  conjghm  13924  ringnegl  14126  ringnegr  14127  ringmneg2  14129  ring1  14134  rdivmuldivd  14220  lmodfopne  14402  lmodvsneg  14407  ioo2bl  15342  ptolemy  15615  coskpi  15639  logbgcd1irr  15758  logbgcd1irraplemap  15760  lgseisenlem3  15871  lgseisenlem4  15872  lgsquadlem1  15876  lgsquadlem2  15877