Theorem 3eqtr3rd 2235

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

Syntax hints:   -> wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  fcofo  5827  fcof1o  5832  frecabcl  6452  nnaword  6564  nninfisol  7192  enomnilem  7197  fodju0  7206  enmkvlem  7220  enwomnilem  7228  pn0sr  7831  negeu  8210  add20  8493  2halves  9211  bcnn  10828  bcpasc  10837  resqrexlemover  11154  fsumneg  11594  geolim  11654  geolim2  11655  mertensabs  11680  sincossq  11891  demoivre  11916  eirraplem  11920  gcdid  12123  gcdmultipled  12130  phiprmpw  12360  pythagtriplem12  12413  expnprm  12491  imasbas  12890  imasplusg  12891  imasmulr  12892  grpinvid1  13124  grpnpcan  13164  grplactcnv  13174  ghmgrp  13188  conjghm  13346  ringnegl  13547  ringnegr  13548  ringmneg2  13550  ring1  13555  rdivmuldivd  13640  lmodfopne  13822  lmodvsneg  13827  ioo2bl  14711  ptolemy  14959  coskpi  14983  logbgcd1irr  15099  logbgcd1irraplemap  15101  lgseisenlem3  15188  lgseisenlem4  15189  lgsquadlem1  15191