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 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  fcofo  5925  fcof1o  5930  frecabcl  6565  nnaword  6679  nninfisol  7332  enomnilem  7337  fodju0  7346  enmkvlem  7360  enwomnilem  7368  pn0sr  7991  negeu  8370  add20  8654  2halves  9373  bcnn  11020  bcpasc  11029  wrdeqs1cat  11305  resqrexlemover  11575  fsumneg  12017  geolim  12077  geolim2  12078  mertensabs  12103  sincossq  12314  demoivre  12339  eirraplem  12343  gcdid  12562  gcdmultipled  12569  phiprmpw  12799  pythagtriplem12  12853  expnprm  12931  imasbas  13395  imasplusg  13396  imasmulr  13397  grpinvid1  13640  grpnpcan  13680  grplactcnv  13690  ghmgrp  13710  conjghm  13868  ringnegl  14070  ringnegr  14071  ringmneg2  14073  ring1  14078  rdivmuldivd  14164  lmodfopne  14346  lmodvsneg  14351  ioo2bl  15281  ptolemy  15554  coskpi  15578  logbgcd1irr  15697  logbgcd1irraplemap  15699  lgseisenlem3  15807  lgseisenlem4  15808  lgsquadlem1  15812  lgsquadlem2  15813