Theorem 3eqtr3rd 2219

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 2212	. 2 |- ( ph -> B = C )
5	1, 4	eqtr3d 2212	1 |- ( ph -> D = C )

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  fcofo  5784  fcof1o  5789  frecabcl  6399  nnaword  6511  nninfisol  7130  enomnilem  7135  fodju0  7144  enmkvlem  7158  enwomnilem  7166  pn0sr  7769  negeu  8147  add20  8430  2halves  9147  bcnn  10736  bcpasc  10745  resqrexlemover  11018  fsumneg  11458  geolim  11518  geolim2  11519  mertensabs  11544  sincossq  11755  demoivre  11779  eirraplem  11783  gcdid  11986  gcdmultipled  11993  phiprmpw  12221  pythagtriplem12  12274  expnprm  12350  imasbas  12727  imasplusg  12728  imasmulr  12729  grpinvid1  12923  grpnpcan  12961  grplactcnv  12971  ghmgrp  12981  ringnegl  13226  rngnegr  13227  ringmneg2  13229  ring1  13234  rdivmuldivd  13311  ioo2bl  14013  ptolemy  14215  coskpi  14239  logbgcd1irr  14355  logbgcd1irraplemap  14357