Theorem 3eqtr3rd 2807

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 2800	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2800	1 ⊢ (𝜑 → 𝐷 = 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755

This theorem is used by:  iunxdif3  5058  fcofo  7319  fcof1oinvd  7324  cantnfp1lem3  9708  fin1a2lem7  10511  prlem934  11145  addlid  11520  addcom  11523  addcomd  11539  negeu  11574  add20  11855  2halves  12591  bcnn  14483  bcpasc  14492  hashfun  14609  hashf1dmrn  14615  ccatf1  14763  wrdeqs1cat  14897  sqreulem  15556  summolem3  15909  fsumneg  15982  geolim  16068  geolim2  16069  mertens  16084  prodmolem3  16129  fallrisefac  16221  bpoly3  16253  sincossq  16373  demoivre  16397  eirrlem  16401  oddpwp1fsum  16591  sadeq  16671  gcdid  16728  gcdmultipled  16736  nn0rppwr  16764  phiprmpw  16982  pythagtriplem12  17033  expnprm  17109  fullresc  18055  grpinvid1  19231  grpnpcan  19271  grplactcnv  19282  ghmgrp  19305  qustrivr  19426  conjghm  19492  odmodnn0  19784  gex1  19835  sylow3lem3  19873  efgredeu  19996  odadd2  20093  gsumval3  20151  pgpfac1lem3a  20322  omndmul2  20377  ringnegl  20563  ringnegr  20564  ringmneg2  20566  rdivmuldivd  20673  imadrhmcl  21084  lmodfopne  21205  lmodvsneg  21211  lssvs0or  21418  lvecinv  21421  lspabs2  21428  zringunit  21802  zringcyg  21805  dvdschrmulg  21864  fermltlchr  21865  sraassab  22206  mplcoe3  22377  mplcoe5  22379  evlvar  22447  psd1  22518  mdetrlin  22947  mdetunilem6  22962  cramerimplem3  23033  cramerimp  23034  paste  23642  tuslem  24615  tususs  24618  ngpds  24953  ioo2bl  25142  ipcau2  25585  dvexp3  26328  rolle  26340  cmvth  26341  dv11cn  26351  lhop  26366  itgsubstlem  26398  itgpowd  26400  ply1divex  26485  fta1glem1  26516  fta1g  26518  dgrnznn  26596  fta1  26659  vieta1lem2  26664  aaliou2  26697  dvtaylp  26727  dvntaylp  26728  taylthlem1  26730  taylthlem2  26731  dvradcnv  26778  ptolemy  26855  coskpi  26881  tanregt0  26897  cxpeq  27115  isosctrlem2  27177  chordthmlem  27190  dcubic  27204  quart1lem  27213  tanatan  27277  atantan  27281  dvatan  27293  birthdaylem2  27310  rlimcxp  27331  jensenlem2  27345  logdiflbnd  27352  emcllem2  27354  lgamgulmlem2  27387  lgamcvg2  27412  basellem8  27445  bclbnd  27637  lgsqr  27708  lgseisenlem3  27734  lgseisenlem4  27735  lgsquadlem1  27737  lgsquadlem2  27738  rpvmasumlem  27844  dchrisumlem1  27846  dchrisum0flblem1  27865  dchrisum0flblem2  27866  dchrisum0re  27870  dchrisum0lem1  27873  mudivsum  27887  mulogsum  27889  vmalogdivsum2  27895  logsqvma2  27900  selberg2lem  27907  logdivbnd  27913  selbergr  27925  selberg3r  27926  pntrlog2bndlem4  27937  pntrlog2bndlem5  27938  pntpbnd2  27944  pw2divscan4d  28860  pw2cutp1  28877  pw2cut2  28878  z12zsodd  28898  miduniq  29187  krippenlem  29192  colperpexlem2  29237  plngrotlem1  29295  ttgcontlem1  29492  brbtwn2  29513  colinearalglem4  29517  axsegconlem9  29533  ax5seglem1  29536  axbtwnid  29547  axeuclidlem  29570  axcontlem2  29573  axcontlem4  29575  grpoinvid1  31160  vcz  31207  hosubsub4  32450  lnop0  32598  branmfn  32737  fressupp  33352  difico  33445  wrdsplex  33573  s3f1  33581  mgcf1o  33634  mndlrinv  33655  cycpmco2lem4  33760  tocyccntz  33775  cyc3genpm  33783  cycpmconjslem2  33786  rlocisunit  33907  kerunit  33956  znfermltl  33992  linds2eq  34006  dvdsruassoi  34009  dvdsruasso  34010  qsdrnglem2  34090  zringfrac  34156  m1pmeq  34187  vr1nz  34195  mplvrpmrhm  34249  esplyfval1  34275  ply1degltdimlem  34324  fedgmullem2  34332  fldextrspunlsplem  34375  constrrtll  34433  constrrtlc1  34434  constrrtcclem  34436  constrrtcc  34437  constrrecl  34471  2sqr3minply  34482  cos9thpiminplylem1  34484  cos9thpiminplylem2  34485  carsggect  35020  carsgclctunlem2  35021  ballotlemfrceq  35231  ballotlemrinv0  35235  hashreprin  35319  hgt750lemb  35355  faclimlem1  36686  irrdifflemf  38438  poimirlem4  38734  poimirlem23  38753  mblfinlem2  38768  voliunnfl  38774  volsupnfl  38775  itg2addnclem3  38783  ftc2nc  38812  dvasin  38814  areacirclem1  38818  areacirclem4  38821  rngonegmn1l  39067  rngonegmn1r  39068  lfl0  40314  latmassOLD  40478  omlmod1i2N  40509  llnexchb2lem  41117  dalawlem3  41122  pmapj2N  41178  osumcllem9N  41213  pexmidlem6N  41224  4atexlemc  41318  cdleme1  41476  cdleme42a  41720  cdlemg13a  41900  cdlemh2  42065  cdlemk1  42080  tendocnv  42270  dihmeetlem12N  42567  dihmeetlem16N  42571  dihmeetlem19N  42574  dochsatshp  42700  dochexmidlem6  42714  mapdval4N  42881  mapdpglem28  42950  mapdpglem31  42952  mapdindp4  42972  hdmap14lem1a  43115  hdmapinvlem4  43170  3rdpwhole  43542  oexpreposd  43572  remul01  43651  sn-negex12  43661  sn-subeu  43671  remulinvcom  43677  sn-0tie0  43708  cnreeu  43747  fltnlta  43867  irrapxlem5  44026  pellfund14  44098  rmxdbl  44139  jm2.22  44195  oaabsb  44488  oaun2  44575  oaun3  44576  sqrtcval  44833  0ellimcdiv  46864  fourierdlem95  47416  etransclem46  47495  sigariz  48078  sin5tlem2  48125  sin5tlem5  48128  cos5t  48130  ichreuopeq  48760  gricushgr  49220  altgsumbc  49669  blengt1fldiv2p1  49910  restclsseplem  50234  cofu1a  50414  cofu2a  50415  uobeqw  50540  swapf2fval  50592  swapf1val  50594  coccom  51052