Theorem 3eqtr3rd 2805

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 2798	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2798	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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  iunxdif3  5055  fcofo  7288  fcof1oinvd  7293  cantnfp1lem3  9665  fin1a2lem7  10465  prlem934  11099  addlid  11474  addcom  11477  addcomd  11493  negeu  11528  add20  11809  2halves  12545  bcnn  14436  bcpasc  14445  hashfun  14562  hashf1dmrn  14568  ccatf1  14716  wrdeqs1cat  14849  sqreulem  15507  summolem3  15860  fsumneg  15933  geolim  16019  geolim2  16020  mertens  16035  prodmolem3  16080  fallrisefac  16172  bpoly3  16204  sincossq  16324  demoivre  16348  eirrlem  16352  oddpwp1fsum  16542  sadeq  16622  gcdid  16679  gcdmultipled  16687  nn0rppwr  16715  phiprmpw  16933  pythagtriplem12  16984  expnprm  17060  fullresc  18006  grpinvid1  19182  grpnpcan  19222  grplactcnv  19233  ghmgrp  19256  qustrivr  19377  conjghm  19443  odmodnn0  19734  gex1  19785  sylow3lem3  19823  efgredeu  19946  odadd2  20043  gsumval3  20101  pgpfac1lem3a  20272  omndmul2  20327  ringnegl  20513  ringnegr  20514  ringmneg2  20516  rdivmuldivd  20623  imadrhmcl  21034  lmodfopne  21155  lmodvsneg  21161  lssvs0or  21368  lvecinv  21371  lspabs2  21378  zringunit  21752  zringcyg  21755  dvdschrmulg  21814  fermltlchr  21815  sraassab  22156  mplcoe3  22327  mplcoe5  22329  evlvar  22397  psd1  22468  mdetrlin  22897  mdetunilem6  22912  cramerimplem3  22983  cramerimp  22984  paste  23592  tuslem  24565  tususs  24568  ngpds  24903  ioo2bl  25092  ipcau2  25535  dvexp3  26278  rolle  26290  cmvth  26291  dv11cn  26301  lhop  26316  itgsubstlem  26348  itgpowd  26350  ply1divex  26435  fta1glem1  26466  fta1g  26468  dgrnznn  26546  fta1  26611  vieta1lem2  26616  aaliou2  26649  dvtaylp  26679  dvntaylp  26680  taylthlem1  26682  taylthlem2  26683  dvradcnv  26730  ptolemy  26807  coskpi  26833  tanregt0  26849  cxpeq  27067  isosctrlem2  27129  chordthmlem  27142  dcubic  27156  quart1lem  27165  tanatan  27229  atantan  27233  dvatan  27245  birthdaylem2  27262  rlimcxp  27283  jensenlem2  27297  logdiflbnd  27304  emcllem2  27306  lgamgulmlem2  27339  lgamcvg2  27364  basellem8  27397  bclbnd  27589  lgsqr  27660  lgseisenlem3  27686  lgseisenlem4  27687  lgsquadlem1  27689  lgsquadlem2  27690  rpvmasumlem  27796  dchrisumlem1  27798  dchrisum0flblem1  27817  dchrisum0flblem2  27818  dchrisum0re  27822  dchrisum0lem1  27825  mudivsum  27839  mulogsum  27841  vmalogdivsum2  27847  logsqvma2  27852  selberg2lem  27859  logdivbnd  27865  selbergr  27877  selberg3r  27878  pntrlog2bndlem4  27889  pntrlog2bndlem5  27890  pntpbnd2  27896  pw2divscan4d  28812  pw2cutp1  28829  pw2cut2  28830  z12zsodd  28850  miduniq  29139  krippenlem  29144  colperpexlem2  29189  plngrotlem1  29247  ttgcontlem1  29444  brbtwn2  29465  colinearalglem4  29469  axsegconlem9  29485  ax5seglem1  29488  axbtwnid  29499  axeuclidlem  29522  axcontlem2  29525  axcontlem4  29527  grpoinvid1  31112  vcz  31159  hosubsub4  32402  lnop0  32550  branmfn  32689  fressupp  33263  difico  33357  wrdsplex  33485  s3f1  33493  mgcf1o  33546  mndlrinv  33567  cycpmco2lem4  33672  tocyccntz  33687  cyc3genpm  33695  cycpmconjslem2  33698  rlocisunit  33819  kerunit  33868  znfermltl  33904  linds2eq  33918  dvdsruassoi  33921  dvdsruasso  33922  qsdrnglem2  34002  zringfrac  34068  m1pmeq  34099  vr1nz  34107  mplvrpmrhm  34161  esplyfval1  34187  ply1degltdimlem  34236  fedgmullem2  34244  fldextrspunlsplem  34287  constrrtll  34345  constrrtlc1  34346  constrrtcclem  34348  constrrtcc  34349  constrrecl  34383  2sqr3minply  34394  cos9thpiminplylem1  34396  cos9thpiminplylem2  34397  carsggect  34933  carsgclctunlem2  34934  ballotlemfrceq  35144  ballotlemrinv0  35148  hashreprin  35232  hgt750lemb  35268  faclimlem1  36477  irrdifflemf  38214  poimirlem4  38510  poimirlem23  38529  mblfinlem2  38544  voliunnfl  38550  volsupnfl  38551  itg2addnclem3  38559  ftc2nc  38588  dvasin  38590  areacirclem1  38594  areacirclem4  38597  rngonegmn1l  38843  rngonegmn1r  38844  lfl0  40090  latmassOLD  40254  omlmod1i2N  40285  llnexchb2lem  40893  dalawlem3  40898  pmapj2N  40954  osumcllem9N  40989  pexmidlem6N  41000  4atexlemc  41094  cdleme1  41252  cdleme42a  41496  cdlemg13a  41676  cdlemh2  41841  cdlemk1  41856  tendocnv  42046  dihmeetlem12N  42343  dihmeetlem16N  42347  dihmeetlem19N  42350  dochsatshp  42476  dochexmidlem6  42490  mapdval4N  42657  mapdpglem28  42726  mapdpglem31  42728  mapdindp4  42748  hdmap14lem1a  42891  hdmapinvlem4  42946  3rdpwhole  43317  oexpreposd  43347  remul01  43426  sn-negex12  43436  sn-subeu  43446  remulinvcom  43452  sn-0tie0  43483  cnreeu  43522  fltnlta  43628  irrapxlem5  43786  pellfund14  43858  rmxdbl  43899  jm2.22  43955  oaabsb  44254  oaun2  44341  oaun3  44342  sqrtcval  44600  0ellimcdiv  46603  fourierdlem95  47155  etransclem46  47234  sigariz  47817  sin5tlem2  47864  sin5tlem5  47867  cos5t  47869  ichreuopeq  48499  gricushgr  48959  altgsumbc  49408  blengt1fldiv2p1  49649  restclsseplem  49967  cofu1a  50146  cofu2a  50147  uobeqw  50271  swapf2fval  50317  swapf1val  50319  coccom  50716