Theorem 3eqtr3rd 2271

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

Syntax hints:   -> wi 4   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  fcofo  5914  fcof1o  5919  frecabcl  6551  nnaword  6665  nninfisol  7311  enomnilem  7316  fodju0  7325  enmkvlem  7339  enwomnilem  7347  pn0sr  7969  negeu  8348  add20  8632  2halves  9351  bcnn  10991  bcpasc  11000  wrdeqs1cat  11267  resqrexlemover  11536  fsumneg  11977  geolim  12037  geolim2  12038  mertensabs  12063  sincossq  12274  demoivre  12299  eirraplem  12303  gcdid  12522  gcdmultipled  12529  phiprmpw  12759  pythagtriplem12  12813  expnprm  12891  imasbas  13355  imasplusg  13356  imasmulr  13357  grpinvid1  13600  grpnpcan  13640  grplactcnv  13650  ghmgrp  13670  conjghm  13828  ringnegl  14029  ringnegr  14030  ringmneg2  14032  ring1  14037  rdivmuldivd  14123  lmodfopne  14305  lmodvsneg  14310  ioo2bl  15240  ptolemy  15513  coskpi  15537  logbgcd1irr  15656  logbgcd1irraplemap  15658  lgseisenlem3  15766  lgseisenlem4  15767  lgsquadlem1  15771  lgsquadlem2  15772