Theorem 3eqtr3rd 2238

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

Syntax hints:   → wi 4   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  fcofo  5832  fcof1o  5837  frecabcl  6458  nnaword  6570  nninfisol  7200  enomnilem  7205  fodju0  7214  enmkvlem  7228  enwomnilem  7236  pn0sr  7840  negeu  8219  add20  8503  2halves  9222  bcnn  10851  bcpasc  10860  resqrexlemover  11177  fsumneg  11618  geolim  11678  geolim2  11679  mertensabs  11704  sincossq  11915  demoivre  11940  eirraplem  11944  gcdid  12163  gcdmultipled  12170  phiprmpw  12400  pythagtriplem12  12454  expnprm  12532  imasbas  12960  imasplusg  12961  imasmulr  12962  grpinvid1  13194  grpnpcan  13234  grplactcnv  13244  ghmgrp  13258  conjghm  13416  ringnegl  13617  ringnegr  13618  ringmneg2  13620  ring1  13625  rdivmuldivd  13710  lmodfopne  13892  lmodvsneg  13897  ioo2bl  14797  ptolemy  15070  coskpi  15094  logbgcd1irr  15213  logbgcd1irraplemap  15215  lgseisenlem3  15323  lgseisenlem4  15324  lgsquadlem1  15328  lgsquadlem2  15329