Theorem 3eqtr3rd 2273

Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)

Hypotheses

Ref	Expression
3eqtr3d.1	|- ( ph -> A = B )
3eqtr3d.2	|- ( ph -> A = C )
3eqtr3d.3	|- ( ph -> B = D )

Assertion

Ref	Expression
3eqtr3rd	|- ( ph -> D = C )

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 |- ( ph -> B = D )
2		3eqtr3d.1	. . 3 |- ( ph -> A = B )
3		3eqtr3d.2	. . 3 |- ( ph -> A = C )
4	2, 3	eqtr3d 2266	. 2 |- ( ph -> B = C )
5	1, 4	eqtr3d 2266	1 |- ( ph -> D = C )

Syntax hints:   -> wi 4   = wceq 1397

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 1495  ax-gen 1497  ax-4 1558  ax-17 1574  ax-ext 2213

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

This theorem is referenced by:  fcofo  5925  fcof1o  5930  frecabcl  6565  nnaword  6679  nninfisol  7332  enomnilem  7337  fodju0  7346  enmkvlem  7360  enwomnilem  7368  pn0sr  7991  negeu  8370  add20  8654  2halves  9373  bcnn  11020  bcpasc  11029  wrdeqs1cat  11305  resqrexlemover  11588  fsumneg  12030  geolim  12090  geolim2  12091  mertensabs  12116  sincossq  12327  demoivre  12352  eirraplem  12356  gcdid  12575  gcdmultipled  12582  phiprmpw  12812  pythagtriplem12  12866  expnprm  12944  imasbas  13408  imasplusg  13409  imasmulr  13410  grpinvid1  13653  grpnpcan  13693  grplactcnv  13703  ghmgrp  13723  conjghm  13881  ringnegl  14083  ringnegr  14084  ringmneg2  14086  ring1  14091  rdivmuldivd  14177  lmodfopne  14359  lmodvsneg  14364  ioo2bl  15294  ptolemy  15567  coskpi  15591  logbgcd1irr  15710  logbgcd1irraplemap  15712  lgseisenlem3  15820  lgseisenlem4  15821  lgsquadlem1  15825  lgsquadlem2  15826