Theorem 3eqtr3rd 2779

Description: A deduction from three chained equalities. (Contributed by NM, 14-Jan-2006.)

Hypotheses

Ref	Expression
3eqtr3d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr3d.2	⊢ (𝜑 → 𝐴 = 𝐶)
3eqtr3d.3	⊢ (𝜑 → 𝐵 = 𝐷)

Assertion

Ref	Expression
3eqtr3rd	⊢ (𝜑 → 𝐷 = 𝐶)

Proof of Theorem 3eqtr3rd

Step	Hyp	Ref	Expression
1		3eqtr3d.3	. 2 ⊢ (𝜑 → 𝐵 = 𝐷)
2		3eqtr3d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3		3eqtr3d.2	. . 3 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	eqtr3d 2772	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2772	1 ⊢ (𝜑 → 𝐷 = 𝐶)

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722

This theorem is referenced by:  iunxdif3  5097  fcofo  7288  fcof1oinvd  7293  cantnfp1lem3  9677  fin1a2lem7  10403  prlem934  11030  addlid  11401  addcom  11404  addcomd  11420  negeu  11454  add20  11730  2halves  12444  bcnn  14276  bcpasc  14285  hashfun  14401  hashf1dmrn  14407  wrdeqs1cat  14674  sqreulem  15310  summolem3  15664  fsumneg  15737  geolim  15820  geolim2  15821  mertens  15836  prodmolem3  15881  fallrisefac  15973  bpoly3  16006  sincossq  16123  demoivre  16147  eirrlem  16151  oddpwp1fsum  16339  sadeq  16417  gcdid  16472  gcdmultipled  16480  phiprmpw  16713  pythagtriplem12  16763  expnprm  16839  fullresc  17805  grpinvid1  18912  grpnpcan  18951  grplactcnv  18962  ghmgrp  18985  conjghm  19163  odmodnn0  19449  gex1  19500  sylow3lem3  19538  efgredeu  19661  odadd2  19758  gsumval3  19816  pgpfac1lem3a  19987  ringnegl  20190  ringnegr  20191  ringmneg2  20193  rdivmuldivd  20304  imadrhmcl  20556  lmodfopne  20654  lmodvsneg  20660  lss0v  20771  lssvs0or  20868  lvecinv  20871  lspabs2  20878  zringunit  21237  zringcyg  21240  sraassab  21641  mplcoe3  21812  mplcoe5  21814  evlvar  21882  mdetrlin  22324  mdetunilem6  22339  cramerimplem3  22407  cramerimp  22408  paste  23018  tuslem  23991  tuslemOLD  23992  tususs  23995  ngpds  24333  ioo2bl  24529  ipcau2  24982  dvexp3  25730  rolle  25742  cmvth  25743  dv11cn  25753  lhop  25768  itgsubstlem  25800  itgpowd  25802  ply1divex  25889  fta1glem1  25918  fta1g  25920  dgrnznn  25996  fta1  26057  vieta1lem2  26060  aaliou2  26089  dvtaylp  26118  dvntaylp  26119  taylthlem1  26121  taylthlem2  26122  dvradcnv  26169  ptolemy  26242  coskpi  26268  tanregt0  26284  cxpeq  26501  isosctrlem2  26560  chordthmlem  26573  dcubic  26587  quart1lem  26596  tanatan  26660  atantan  26664  dvatan  26676  birthdaylem2  26693  rlimcxp  26714  jensenlem2  26728  logdiflbnd  26735  emcllem2  26737  lgamgulmlem2  26770  lgamcvg2  26795  basellem8  26828  bclbnd  27019  lgsqr  27090  lgseisenlem3  27116  lgseisenlem4  27117  lgsquadlem1  27119  lgsquadlem2  27120  rpvmasumlem  27226  dchrisumlem1  27228  dchrisum0flblem1  27247  dchrisum0flblem2  27248  dchrisum0re  27252  dchrisum0lem1  27255  mudivsum  27269  mulogsum  27271  vmalogdivsum2  27277  logsqvma2  27282  selberg2lem  27289  logdivbnd  27295  selbergr  27307  selberg3r  27308  pntrlog2bndlem4  27319  pntrlog2bndlem5  27320  pntpbnd2  27326  miduniq  28203  krippenlem  28208  colperpexlem2  28249  ttgcontlem1  28409  brbtwn2  28430  colinearalglem4  28434  axsegconlem9  28450  ax5seglem1  28453  axbtwnid  28464  axeuclidlem  28487  axcontlem2  28490  axcontlem4  28492  grpoinvid1  30048  vcz  30095  hosubsub4  31338  lnop0  31486  branmfn  31625  fressupp  32177  difico  32261  wrdsplex  32371  s3f1  32380  ccatf1  32382  mgcf1o  32440  omndmul2  32500  cycpmco2lem4  32558  tocyccntz  32573  cyc3genpm  32581  cycpmconjslem2  32584  dvdschrmulg  32650  kerunit  32707  qustrivr  32751  fermltlchr  32752  znfermltl  32753  dvdsruassoi  32763  dvdsruasso  32764  linds2eq  32771  qsdrnglem2  32884  ply1degltdimlem  32995  fedgmullem2  33003  carsggect  33615  carsgclctunlem2  33616  ballotlemfrceq  33825  ballotlemrinv0  33829  hashreprin  33930  hgt750lemb  33966  faclimlem1  35017  gg-cmvth  35466  irrdifflemf  36509  poimirlem4  36795  poimirlem23  36814  mblfinlem2  36829  voliunnfl  36835  volsupnfl  36836  itg2addnclem3  36844  ftc2nc  36873  dvasin  36875  areacirclem1  36879  areacirclem4  36882  rngonegmn1l  37112  rngonegmn1r  37113  lfl0  38238  latmassOLD  38402  omlmod1i2N  38433  llnexchb2lem  39042  dalawlem3  39047  pmapj2N  39103  osumcllem9N  39138  pexmidlem6N  39149  4atexlemc  39243  cdleme1  39401  cdleme42a  39645  cdlemg13a  39825  cdlemh2  39990  cdlemk1  40005  tendocnv  40195  dihmeetlem12N  40492  dihmeetlem16N  40496  dihmeetlem19N  40499  dochsatshp  40625  dochexmidlem6  40639  mapdval4N  40806  mapdpglem28  40875  mapdpglem31  40877  mapdindp4  40897  hdmap14lem1a  41040  hdmapinvlem4  41095  oexpreposd  41514  nn0rppwr  41526  sn-00idlem3  41575  remul01  41582  sn-subeu  41601  remulinvcom  41607  sn-0tie0  41614  cnreeu  41643  fltnlta  41707  irrapxlem5  41866  pellfund14  41938  rmxdbl  41980  jm2.22  42036  oaabsb  42346  oaun2  42433  oaun3  42434  sqrtcval  42694  0ellimcdiv  44663  fourierdlem95  45215  etransclem46  45294  sigariz  45877  ichreuopeq  46439  isomushgr  46792  altgsumbc  47116  blengt1fldiv2p1  47366  restclsseplem  47634