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  6675  nnaword  6789  nninfisol  7480  enomnilem  7485  fodju0  7494  enmkvlem  7508  enwomnilem  7516  pn0sr  8145  negeu  8525  add20  8810  2halves  9546  lincmble  10423  bcnn  11217  bcpasc  11226  wrdeqs1cat  11514  resqrexlemover  11798  fsumneg  12243  geolim  12303  geolim2  12304  mertensabs  12329  sincossq  12540  demoivre  12565  eirraplem  12569  gcdid  12788  gcdmultipled  12795  phiprmpw  13029  pythagtriplem12  13083  expnprm  13161  ballotfilemrinv0  13334  imasbas  13687  imasplusg  13688  imasmulr  13689  grpinvid1  13916  grpnpcan  13956  grplactcnv  13966  ghmgrp  13980  conjghm  14138  ringnegl  14463  ringnegr  14464  ringmneg2  14466  ring1  14471  rdivmuldivd  14560  lmodfopne  14772  lmodvsneg  14777  ioo2bl  15810  ptolemy  16084  coskpi  16108  logbgcd1irr  16236  logbgcd1irraplemap  16238  birthdaylem2  16259  bclbnd  16340  lgseisenlem3  16429  lgseisenlem4  16430  lgsquadlem1  16434  lgsquadlem2  16435