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  5920  fcof1o  5925  frecabcl  6560  nnaword  6674  nninfisol  7323  enomnilem  7328  fodju0  7337  enmkvlem  7351  enwomnilem  7359  pn0sr  7981  negeu  8360  add20  8644  2halves  9363  bcnn  11009  bcpasc  11018  wrdeqs1cat  11291  resqrexlemover  11561  fsumneg  12002  geolim  12062  geolim2  12063  mertensabs  12088  sincossq  12299  demoivre  12324  eirraplem  12328  gcdid  12547  gcdmultipled  12554  phiprmpw  12784  pythagtriplem12  12838  expnprm  12916  imasbas  13380  imasplusg  13381  imasmulr  13382  grpinvid1  13625  grpnpcan  13665  grplactcnv  13675  ghmgrp  13695  conjghm  13853  ringnegl  14054  ringnegr  14055  ringmneg2  14057  ring1  14062  rdivmuldivd  14148  lmodfopne  14330  lmodvsneg  14335  ioo2bl  15265  ptolemy  15538  coskpi  15562  logbgcd1irr  15681  logbgcd1irraplemap  15683  lgseisenlem3  15791  lgseisenlem4  15792  lgsquadlem1  15796  lgsquadlem2  15797