Theorem 3eqtr3rd 2276

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

Syntax hints:   -> wi 4   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  fcofo  5959  fcof1o  5964  frecabcl  6632  nnaword  6746  nninfisol  7426  enomnilem  7431  fodju0  7440  enmkvlem  7454  enwomnilem  7462  pn0sr  8088  negeu  8466  add20  8750  2halves  9469  lincmble  10340  bcnn  11123  bcpasc  11132  wrdeqs1cat  11416  resqrexlemover  11699  fsumneg  12141  geolim  12201  geolim2  12202  mertensabs  12227  sincossq  12438  demoivre  12463  eirraplem  12467  gcdid  12686  gcdmultipled  12693  phiprmpw  12923  pythagtriplem12  12977  expnprm  13055  imasbas  13537  imasplusg  13538  imasmulr  13539  grpinvid1  13782  grpnpcan  13822  grplactcnv  13832  ghmgrp  13852  conjghm  14010  ringnegl  14212  ringnegr  14213  ringmneg2  14215  ring1  14220  rdivmuldivd  14306  lmodfopne  14491  lmodvsneg  14496  ioo2bl  15433  ptolemy  15706  coskpi  15730  logbgcd1irr  15849  logbgcd1irraplemap  15851  lgseisenlem3  15962  lgseisenlem4  15963  lgsquadlem1  15967  lgsquadlem2  15968