Theorem 3eqtr3rd 2271

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

Syntax hints:   → wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  fcofo  5920  fcof1o  5925  frecabcl  6560  nnaword  6674  nninfisol  7326  enomnilem  7331  fodju0  7340  enmkvlem  7354  enwomnilem  7362  pn0sr  7984  negeu  8363  add20  8647  2halves  9366  bcnn  11012  bcpasc  11021  wrdeqs1cat  11294  resqrexlemover  11564  fsumneg  12005  geolim  12065  geolim2  12066  mertensabs  12091  sincossq  12302  demoivre  12327  eirraplem  12331  gcdid  12550  gcdmultipled  12557  phiprmpw  12787  pythagtriplem12  12841  expnprm  12919  imasbas  13383  imasplusg  13384  imasmulr  13385  grpinvid1  13628  grpnpcan  13668  grplactcnv  13678  ghmgrp  13698  conjghm  13856  ringnegl  14057  ringnegr  14058  ringmneg2  14060  ring1  14065  rdivmuldivd  14151  lmodfopne  14333  lmodvsneg  14338  ioo2bl  15268  ptolemy  15541  coskpi  15565  logbgcd1irr  15684  logbgcd1irraplemap  15686  lgseisenlem3  15794  lgseisenlem4  15795  lgsquadlem1  15799  lgsquadlem2  15800