Theorem 3eqtr3rd 2784

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732

This theorem is referenced by:  iunxdif3  5031  fcofo  7239  fcof1oinvd  7244  cantnfp1lem3  9599  fin1a2lem7  10326  prlem934  10954  addlid  11327  addcom  11330  addcomd  11346  negeu  11381  add20  11660  2halves  12393  bcnn  14272  bcpasc  14281  hashfun  14397  hashf1dmrn  14403  wrdeqs1cat  14680  sqreulem  15320  summolem3  15674  fsumneg  15747  geolim  15833  geolim2  15834  mertens  15849  prodmolem3  15896  fallrisefac  15988  bpoly3  16021  sincossq  16141  demoivre  16165  eirrlem  16169  oddpwp1fsum  16359  sadeq  16439  gcdid  16494  gcdmultipled  16501  nn0rppwr  16528  phiprmpw  16744  pythagtriplem12  16795  expnprm  16871  fullresc  17816  grpinvid1  18965  grpnpcan  19006  grplactcnv  19017  ghmgrp  19040  conjghm  19222  odmodnn0  19513  gex1  19564  sylow3lem3  19602  efgredeu  19725  odadd2  19822  gsumval3  19880  pgpfac1lem3a  20051  omndmul2  20106  ringnegl  20281  ringnegr  20282  ringmneg2  20284  rdivmuldivd  20391  imadrhmcl  20776  lmodfopne  20897  lmodvsneg  20903  lssvs0or  21110  lvecinv  21113  lspabs2  21120  zringunit  21448  zringcyg  21451  dvdschrmulg  21510  fermltlchr  21511  sraassab  21850  mplcoe3  22021  mplcoe5  22023  evlvar  22091  psd1  22162  mdetrlin  22592  mdetunilem6  22607  cramerimplem3  22675  cramerimp  22676  paste  23284  tuslem  24256  tususs  24259  ngpds  24594  ioo2bl  24783  ipcau2  25226  dvexp3  25970  rolle  25982  cmvth  25983  dv11cn  25993  lhop  26008  itgsubstlem  26040  itgpowd  26042  ply1divex  26127  fta1glem1  26158  fta1g  26160  dgrnznn  26237  fta1  26299  vieta1lem2  26302  aaliou2  26331  dvtaylp  26360  dvntaylp  26361  taylthlem1  26363  taylthlem2  26364  dvradcnv  26411  ptolemy  26485  coskpi  26512  tanregt0  26528  cxpeq  26746  isosctrlem2  26808  chordthmlem  26821  dcubic  26835  quart1lem  26844  tanatan  26908  atantan  26912  dvatan  26924  birthdaylem2  26941  rlimcxp  26962  jensenlem2  26976  logdiflbnd  26983  emcllem2  26985  lgamgulmlem2  27018  lgamcvg2  27043  basellem8  27076  bclbnd  27268  lgsqr  27339  lgseisenlem3  27365  lgseisenlem4  27366  lgsquadlem1  27368  lgsquadlem2  27369  rpvmasumlem  27475  dchrisumlem1  27477  dchrisum0flblem1  27496  dchrisum0flblem2  27497  dchrisum0re  27501  dchrisum0lem1  27504  mudivsum  27518  mulogsum  27520  vmalogdivsum2  27526  logsqvma2  27531  selberg2lem  27538  logdivbnd  27544  selbergr  27556  selberg3r  27557  pntrlog2bndlem4  27568  pntrlog2bndlem5  27569  pntpbnd2  27575  pw2divscan4d  28461  pw2cutp1  28478  pw2cut2  28479  z12zsodd  28499  miduniq  28778  krippenlem  28783  colperpexlem2  28824  ttgcontlem1  28978  brbtwn2  28999  colinearalglem4  29003  axsegconlem9  29019  ax5seglem1  29022  axbtwnid  29033  axeuclidlem  29056  axcontlem2  29059  axcontlem4  29061  grpoinvid1  30624  vcz  30671  hosubsub4  31914  lnop0  32062  branmfn  32201  fressupp  32787  difico  32882  wrdsplex  33022  s3f1  33033  ccatf1  33035  mgcf1o  33089  mndlrinv  33110  cycpmco2lem4  33217  tocyccntz  33232  cyc3genpm  33240  cycpmconjslem2  33243  kerunit  33415  qustrivr  33455  znfermltl  33456  linds2eq  33471  dvdsruassoi  33474  dvdsruasso  33475  qsdrnglem2  33586  zringfrac  33644  m1pmeq  33675  vr1nz  33683  mplvrpmrhm  33738  esplyfval1  33764  ply1degltdimlem  33813  fedgmullem2  33821  fldextrspunlsplem  33864  constrrtll  33922  constrrtlc1  33923  constrrtcclem  33925  constrrtcc  33926  constrrecl  33960  2sqr3minply  33971  cos9thpiminplylem1  33973  cos9thpiminplylem2  33974  carsggect  34509  carsgclctunlem2  34510  ballotlemfrceq  34720  ballotlemrinv0  34724  hashreprin  34811  hgt750lemb  34847  faclimlem1  35978  irrdifflemf  37692  poimirlem4  37998  poimirlem23  38017  mblfinlem2  38032  voliunnfl  38038  volsupnfl  38039  itg2addnclem3  38047  ftc2nc  38076  dvasin  38078  areacirclem1  38082  areacirclem4  38085  rngonegmn1l  38315  rngonegmn1r  38316  lfl0  39564  latmassOLD  39728  omlmod1i2N  39759  llnexchb2lem  40367  dalawlem3  40372  pmapj2N  40428  osumcllem9N  40463  pexmidlem6N  40474  4atexlemc  40568  cdleme1  40726  cdleme42a  40970  cdlemg13a  41150  cdlemh2  41315  cdlemk1  41330  tendocnv  41520  dihmeetlem12N  41817  dihmeetlem16N  41821  dihmeetlem19N  41824  dochsatshp  41950  dochexmidlem6  41964  mapdval4N  42131  mapdpglem28  42200  mapdpglem31  42202  mapdindp4  42222  hdmap14lem1a  42365  hdmapinvlem4  42420  3rdpwhole  42776  oexpreposd  42806  remul01  42891  sn-negex12  42901  sn-subeu  42911  remulinvcom  42917  sn-0tie0  42948  cnreeu  42987  fltnlta  43120  irrapxlem5  43278  pellfund14  43350  rmxdbl  43391  jm2.22  43447  oaabsb  43746  oaun2  43833  oaun3  43834  sqrtcval  44092  0ellimcdiv  46099  fourierdlem95  46651  etransclem46  46730  sigariz  47313  sin5tlem2  47344  sin5tlem5  47347  cos5t  47349  ichreuopeq  47955  gricushgr  48415  altgsumbc  48850  blengt1fldiv2p1  49091  restclsseplem  49412  cofu1a  49591  cofu2a  49592  uobeqw  49716  swapf2fval  49762  swapf1val  49764  coccom  50161