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  7473  enomnilem  7478  fodju0  7487  enmkvlem  7501  enwomnilem  7509  pn0sr  8138  negeu  8517  add20  8802  2halves  9536  lincmble  10408  bcnn  11197  bcpasc  11206  wrdeqs1cat  11494  resqrexlemover  11778  fsumneg  12220  geolim  12280  geolim2  12281  mertensabs  12306  sincossq  12517  demoivre  12542  eirraplem  12546  gcdid  12765  gcdmultipled  12772  phiprmpw  13002  pythagtriplem12  13056  expnprm  13134  ballotfilemrinv0  13278  imasbas  13630  imasplusg  13631  imasmulr  13632  grpinvid1  13859  grpnpcan  13899  grplactcnv  13909  ghmgrp  13923  conjghm  14081  ringnegl  14358  ringnegr  14359  ringmneg2  14361  ring1  14366  rdivmuldivd  14453  lmodfopne  14665  lmodvsneg  14670  ioo2bl  15654  ptolemy  15928  coskpi  15952  logbgcd1irr  16075  logbgcd1irraplemap  16077  birthdaylem2  16094  bclbnd  16127  lgseisenlem3  16203  lgseisenlem4  16204  lgsquadlem1  16208  lgsquadlem2  16209