Theorem 3eqtr3rd 2780

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2723

This theorem is referenced by:  iunxdif3  5091  fcofo  7270  fcof1oinvd  7275  cantnfp1lem3  9657  fin1a2lem7  10383  prlem934  11010  addlid  11379  addcom  11382  addcomd  11398  negeu  11432  add20  11708  2halves  12422  bcnn  14254  bcpasc  14263  hashfun  14379  hashf1dmrn  14385  wrdeqs1cat  14652  sqreulem  15288  summolem3  15642  fsumneg  15715  geolim  15798  geolim2  15799  mertens  15814  prodmolem3  15859  fallrisefac  15951  bpoly3  15984  sincossq  16101  demoivre  16125  eirrlem  16129  oddpwp1fsum  16317  sadeq  16395  gcdid  16450  gcdmultipled  16458  phiprmpw  16691  pythagtriplem12  16741  expnprm  16817  fullresc  17783  grpinvid1  18851  grpnpcan  18889  grplactcnv  18900  ghmgrp  18921  conjghm  19089  odmodnn0  19372  gex1  19423  sylow3lem3  19461  efgredeu  19584  odadd2  19677  gsumval3  19734  pgpfac1lem3a  19905  ringnegl  20071  ringnegr  20072  ringmneg2  20074  rdivmuldivd  20177  imadrhmcl  20362  lmodfopne  20459  lmodvsneg  20465  lss0v  20576  lssvs0or  20672  lvecinv  20675  lspabs2  20682  zringunit  20969  zringcyg  20972  mplcoe3  21521  mplcoe5  21523  evlvar  21592  mdetrlin  22033  mdetunilem6  22048  cramerimplem3  22116  cramerimp  22117  paste  22727  tuslem  23700  tuslemOLD  23701  tususs  23704  ngpds  24042  ioo2bl  24238  ipcau2  24680  dvexp3  25424  rolle  25436  cmvth  25437  dv11cn  25447  lhop  25462  itgsubstlem  25494  itgpowd  25496  ply1divex  25583  fta1glem1  25612  fta1g  25614  dgrnznn  25690  fta1  25750  vieta1lem2  25753  aaliou2  25782  dvtaylp  25811  dvntaylp  25812  taylthlem1  25814  taylthlem2  25815  dvradcnv  25862  ptolemy  25935  coskpi  25961  tanregt0  25977  cxpeq  26192  isosctrlem2  26251  chordthmlem  26264  dcubic  26278  quart1lem  26287  tanatan  26351  atantan  26355  dvatan  26367  birthdaylem2  26384  rlimcxp  26405  jensenlem2  26419  logdiflbnd  26426  emcllem2  26428  lgamgulmlem2  26461  lgamcvg2  26486  basellem8  26519  bclbnd  26710  lgsqr  26781  lgseisenlem3  26807  lgseisenlem4  26808  lgsquadlem1  26810  lgsquadlem2  26811  rpvmasumlem  26917  dchrisumlem1  26919  dchrisum0flblem1  26938  dchrisum0flblem2  26939  dchrisum0re  26943  dchrisum0lem1  26946  mudivsum  26960  mulogsum  26962  vmalogdivsum2  26968  logsqvma2  26973  selberg2lem  26980  logdivbnd  26986  selbergr  26998  selberg3r  26999  pntrlog2bndlem4  27010  pntrlog2bndlem5  27011  pntpbnd2  27017  miduniq  27801  krippenlem  27806  colperpexlem2  27847  ttgcontlem1  28007  brbtwn2  28028  colinearalglem4  28032  axsegconlem9  28048  ax5seglem1  28051  axbtwnid  28062  axeuclidlem  28085  axcontlem2  28088  axcontlem4  28090  grpoinvid1  29644  vcz  29691  hosubsub4  30934  lnop0  31082  branmfn  31221  fressupp  31781  difico  31865  wrdsplex  31975  s3f1  31984  ccatf1  31986  mgcf1o  32044  omndmul2  32101  cycpmco2lem4  32159  tocyccntz  32174  cyc3genpm  32182  cycpmconjslem2  32185  dvdschrmulg  32248  kerunit  32299  qustrivr  32339  fermltlchr  32340  znfermltl  32341  linds2eq  32355  qsdrnglem2  32456  ply1degltdimlem  32545  fedgmullem2  32553  carsggect  33148  carsgclctunlem2  33149  ballotlemfrceq  33358  ballotlemrinv0  33362  hashreprin  33463  hgt750lemb  33499  faclimlem1  34543  irrdifflemf  36010  poimirlem4  36296  poimirlem23  36315  mblfinlem2  36330  voliunnfl  36336  volsupnfl  36337  itg2addnclem3  36345  ftc2nc  36374  dvasin  36376  areacirclem1  36380  areacirclem4  36383  rngonegmn1l  36614  rngonegmn1r  36615  lfl0  37740  latmassOLD  37904  omlmod1i2N  37935  llnexchb2lem  38544  dalawlem3  38549  pmapj2N  38605  osumcllem9N  38640  pexmidlem6N  38651  4atexlemc  38745  cdleme1  38903  cdleme42a  39147  cdlemg13a  39327  cdlemh2  39492  cdlemk1  39507  tendocnv  39697  dihmeetlem12N  39994  dihmeetlem16N  39998  dihmeetlem19N  40001  dochsatshp  40127  dochexmidlem6  40141  mapdval4N  40308  mapdpglem28  40377  mapdpglem31  40379  mapdindp4  40399  hdmap14lem1a  40542  hdmapinvlem4  40597  oexpreposd  40993  nn0rppwr  41005  sn-00idlem3  41055  remul01  41062  sn-subeu  41081  remulinvcom  41087  sn-0tie0  41094  cnreeu  41123  fltnlta  41187  irrapxlem5  41335  pellfund14  41407  rmxdbl  41449  jm2.22  41505  oaabsb  41815  oaun2  41902  oaun3  41903  sqrtcval  42163  0ellimcdiv  44138  fourierdlem95  44690  etransclem46  44769  sigariz  45352  ichreuopeq  45913  isomushgr  46266  altgsumbc  46676  blengt1fldiv2p1  46927  restclsseplem  47195