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 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2213

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

This theorem is referenced by:  fcofo  5935  fcof1o  5940  frecabcl  6608  nnaword  6722  nninfisol  7375  enomnilem  7380  fodju0  7389  enmkvlem  7403  enwomnilem  7411  pn0sr  8034  negeu  8412  add20  8696  2halves  9415  lincmble  10283  bcnn  11065  bcpasc  11074  wrdeqs1cat  11350  resqrexlemover  11633  fsumneg  12075  geolim  12135  geolim2  12136  mertensabs  12161  sincossq  12372  demoivre  12397  eirraplem  12401  gcdid  12620  gcdmultipled  12627  phiprmpw  12857  pythagtriplem12  12911  expnprm  12989  imasbas  13453  imasplusg  13454  imasmulr  13455  grpinvid1  13698  grpnpcan  13738  grplactcnv  13748  ghmgrp  13768  conjghm  13926  ringnegl  14128  ringnegr  14129  ringmneg2  14131  ring1  14136  rdivmuldivd  14222  lmodfopne  14405  lmodvsneg  14410  ioo2bl  15345  ptolemy  15618  coskpi  15642  logbgcd1irr  15761  logbgcd1irraplemap  15763  lgseisenlem3  15874  lgseisenlem4  15875  lgsquadlem1  15879  lgsquadlem2  15880