Theorem 3eqtr3rd 2665

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

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  iunxdif3  4606  fcofo  6543  fcof1oinvd  6548  cantnfp1lem3  8577  fin1a2lem7  9228  prlem934  9855  addid2  10219  addcom  10222  addcomd  10238  negeu  10271  add20  10540  2halves  11260  bcnn  13099  bcpasc  13108  hashfun  13224  wrdeqs1cat  13474  sqreulem  14099  summolem3  14445  fsumneg  14519  geolim  14601  geolim2  14602  mertens  14618  prodmolem3  14663  fallrisefac  14756  bpoly3  14789  sincossq  14906  demoivre  14930  eirrlem  14932  oddpwp1fsum  15115  sadeq  15194  gcdid  15248  phiprmpw  15481  pythagtriplem12  15531  expnprm  15606  fullresc  16511  grpinvid1  17470  grpnpcan  17507  grplactcnv  17518  ghmgrp  17539  conjghm  17691  odmodnn0  17959  gex1  18006  sylow3lem3  18044  efgredeu  18165  odadd2  18252  gsumval3  18308  pgpfac1lem3a  18475  ringnegl  18594  rngnegr  18595  ringmneg2  18597  lmodfopne  18901  lmodvsneg  18907  lss0v  19016  lssvs0or  19110  lvecinv  19113  lspabs2  19120  mplcoe3  19466  mplcoe5  19468  evlvar  19529  zringunit  19836  zringcyg  19839  mdetrlin  20408  mdetunilem6  20423  cramerimplem3  20491  cramerimp  20492  paste  21098  tuslem  22071  tususs  22074  ngpds  22408  ioo2bl  22596  ipcau2  23033  dvexp3  23741  rolle  23753  cmvth  23754  dv11cn  23764  lhop  23779  itgsubstlem  23811  ply1divex  23896  fta1glem1  23925  fta1g  23927  dgrnznn  24003  fta1  24063  vieta1lem2  24066  aaliou2  24095  dvtaylp  24124  dvntaylp  24125  taylthlem1  24127  taylthlem2  24128  dvradcnv  24175  ptolemy  24248  coskpi  24272  tanregt0  24285  cxpeq  24498  isosctrlem2  24549  chordthmlem  24559  dcubic  24573  quart1lem  24582  tanatan  24646  atantan  24650  dvatan  24662  birthdaylem2  24679  rlimcxp  24700  jensenlem2  24714  logdiflbnd  24721  emcllem2  24723  lgamgulmlem2  24756  lgamcvg2  24781  basellem8  24814  bclbnd  25005  lgsqr  25076  lgseisenlem3  25102  lgseisenlem4  25103  lgsquadlem1  25105  lgsquadlem2  25106  rpvmasumlem  25176  dchrisumlem1  25178  dchrisum0flblem1  25197  dchrisum0flblem2  25198  dchrisum0re  25202  dchrisum0lem1  25205  mudivsum  25219  mulogsum  25221  vmalogdivsum2  25227  logsqvma2  25232  selberg2lem  25239  logdivbnd  25245  selbergr  25257  selberg3r  25258  pntrlog2bndlem4  25269  pntrlog2bndlem5  25270  pntpbnd2  25276  miduniq  25580  krippenlem  25585  colperpexlem2  25623  ttgcontlem1  25765  brbtwn2  25785  colinearalglem4  25789  axsegconlem9  25805  ax5seglem1  25808  axbtwnid  25819  axeuclidlem  25842  axcontlem2  25845  axcontlem4  25847  clwwlksel  26914  grpoinvid1  27382  vcz  27430  hosubsub4  28677  lnop0  28825  branmfn  28964  difico  29545  omndmul2  29712  rdivmuldivd  29791  kerunit  29823  carsggect  30380  carsgclctunlem2  30381  ballotlemfrceq  30590  ballotlemrinv0  30594  wrdsplex  30618  hashreprin  30698  hgt750lemb  30734  faclimlem1  31629  poimirlem4  33413  poimirlem23  33432  mblfinlem2  33447  voliunnfl  33453  volsupnfl  33454  itg2addnclem3  33463  ftc2nc  33494  dvasin  33496  areacirclem1  33500  areacirclem4  33503  rngonegmn1l  33740  rngonegmn1r  33741  lfl0  34352  latmassOLD  34516  omlmod1i2N  34547  llnexchb2lem  35154  dalawlem3  35159  pmapj2N  35215  osumcllem9N  35250  pexmidlem6N  35261  4atexlemc  35355  cdleme1  35514  cdleme42a  35759  cdlemg13a  35939  cdlemh2  36104  cdlemk1  36119  tendocnv  36310  dihmeetlem12N  36607  dihmeetlem16N  36611  dihmeetlem19N  36614  dochsatshp  36740  dochexmidlem6  36754  mapdval4N  36921  mapdpglem28  36990  mapdpglem31  36992  mapdindp4  37012  hdmap14lem1a  37158  hdmapinvlem4  37213  irrapxlem5  37390  pellfund14  37462  rmxdbl  37504  jm2.22  37562  itgpowd  37800  0ellimcdiv  39881  fourierdlem95  40418  etransclem46  40497  sigariz  41052  altgsumbc  42130  blengt1fldiv2p1  42387