Theorem 3eqtr3rd 2238

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 2231	. 2 |- ( ph -> B = C )
5	1, 4	eqtr3d 2231	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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  fcofo  5834  fcof1o  5839  frecabcl  6466  nnaword  6578  nninfisol  7208  enomnilem  7213  fodju0  7222  enmkvlem  7236  enwomnilem  7244  pn0sr  7857  negeu  8236  add20  8520  2halves  9239  bcnn  10868  bcpasc  10877  resqrexlemover  11194  fsumneg  11635  geolim  11695  geolim2  11696  mertensabs  11721  sincossq  11932  demoivre  11957  eirraplem  11961  gcdid  12180  gcdmultipled  12187  phiprmpw  12417  pythagtriplem12  12471  expnprm  12549  imasbas  13011  imasplusg  13012  imasmulr  13013  grpinvid1  13256  grpnpcan  13296  grplactcnv  13306  ghmgrp  13326  conjghm  13484  ringnegl  13685  ringnegr  13686  ringmneg2  13688  ring1  13693  rdivmuldivd  13778  lmodfopne  13960  lmodvsneg  13965  ioo2bl  14895  ptolemy  15168  coskpi  15192  logbgcd1irr  15311  logbgcd1irraplemap  15313  lgseisenlem3  15421  lgseisenlem4  15422  lgsquadlem1  15426  lgsquadlem2  15427