Theorem 3eqtr3rd 2219

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  fcofo  5788  fcof1o  5793  frecabcl  6403  nnaword  6515  nninfisol  7134  enomnilem  7139  fodju0  7148  enmkvlem  7162  enwomnilem  7170  pn0sr  7773  negeu  8151  add20  8434  2halves  9151  bcnn  10740  bcpasc  10749  resqrexlemover  11022  fsumneg  11462  geolim  11522  geolim2  11523  mertensabs  11548  sincossq  11759  demoivre  11783  eirraplem  11787  gcdid  11990  gcdmultipled  11997  phiprmpw  12225  pythagtriplem12  12278  expnprm  12354  imasbas  12734  imasplusg  12735  imasmulr  12736  grpinvid1  12931  grpnpcan  12969  grplactcnv  12979  ghmgrp  12991  ringnegl  13239  ringnegr  13240  ringmneg2  13242  ring1  13247  rdivmuldivd  13324  lmodfopne  13427  lmodvsneg  13432  ioo2bl  14204  ptolemy  14406  coskpi  14430  logbgcd1irr  14546  logbgcd1irraplemap  14548