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  5990  fcof1o  5995  frecabcl  6670  nnaword  6784  nninfisol  7474  enomnilem  7479  fodju0  7488  enmkvlem  7502  enwomnilem  7510  pn0sr  8139  negeu  8519  add20  8804  2halves  9539  lincmble  10417  bcnn  11210  bcpasc  11219  wrdeqs1cat  11507  resqrexlemover  11791  fsumneg  12236  geolim  12296  geolim2  12297  mertensabs  12322  sincossq  12533  demoivre  12558  eirraplem  12562  gcdid  12781  gcdmultipled  12788  phiprmpw  13022  pythagtriplem12  13076  expnprm  13154  ballotfilemrinv0  13327  imasbas  13679  imasplusg  13680  imasmulr  13681  grpinvid1  13908  grpnpcan  13948  grplactcnv  13958  ghmgrp  13972  conjghm  14130  ringnegl  14407  ringnegr  14408  ringmneg2  14410  ring1  14415  rdivmuldivd  14502  lmodfopne  14714  lmodvsneg  14719  ioo2bl  15704  ptolemy  15978  coskpi  16002  logbgcd1irr  16125  logbgcd1irraplemap  16127  birthdaylem2  16148  bclbnd  16229  lgseisenlem3  16313  lgseisenlem4  16314  lgsquadlem1  16318  lgsquadlem2  16319