Theorem 3eqtr3rd 2280

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

This proof depends on syntax axioms:   → wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  fcofo  5993  fcof1o  5998  frecabcl  6674  nnaword  6788  nninfisol  7480  enomnilem  7485  fodju0  7494  enmkvlem  7508  enwomnilem  7516  pn0sr  8145  negeu  8525  add20  8810  2halves  9546  lincmble  10424  bcnn  11218  bcpasc  11227  wrdeqs1cat  11515  resqrexlemover  11799  fsumneg  12244  geolim  12304  geolim2  12305  mertensabs  12330  sincossq  12541  demoivre  12566  eirraplem  12570  gcdid  12789  gcdmultipled  12796  phiprmpw  13030  pythagtriplem12  13084  expnprm  13162  ballotfilemrinv0  13335  imasbas  13688  imasplusg  13689  imasmulr  13690  grpinvid1  13917  grpnpcan  13957  grplactcnv  13967  ghmgrp  13981  conjghm  14139  ringnegl  14464  ringnegr  14465  ringmneg2  14467  ring1  14472  rdivmuldivd  14561  lmodfopne  14773  lmodvsneg  14778  ioo2bl  15789  ptolemy  16063  coskpi  16087  logbgcd1irr  16215  logbgcd1irraplemap  16217  birthdaylem2  16238  bclbnd  16319  lgseisenlem3  16408  lgseisenlem4  16409  lgsquadlem1  16413  lgsquadlem2  16414