Theorem 3eqtr3rd 2773

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

Syntax hints:   → wi 4   = wceq 1540

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  iunxdif3  5047  fcofo  7229  fcof1oinvd  7234  cantnfp1lem3  9595  fin1a2lem7  10319  prlem934  10946  addlid  11317  addcom  11320  addcomd  11336  negeu  11371  add20  11650  2halves  12360  bcnn  14237  bcpasc  14246  hashfun  14362  hashf1dmrn  14368  wrdeqs1cat  14644  sqreulem  15285  summolem3  15639  fsumneg  15712  geolim  15795  geolim2  15796  mertens  15811  prodmolem3  15858  fallrisefac  15950  bpoly3  15983  sincossq  16103  demoivre  16127  eirrlem  16131  oddpwp1fsum  16321  sadeq  16401  gcdid  16456  gcdmultipled  16463  nn0rppwr  16490  phiprmpw  16705  pythagtriplem12  16756  expnprm  16832  fullresc  17776  grpinvid1  18888  grpnpcan  18929  grplactcnv  18940  ghmgrp  18963  conjghm  19146  odmodnn0  19437  gex1  19488  sylow3lem3  19526  efgredeu  19649  odadd2  19746  gsumval3  19804  pgpfac1lem3a  19975  omndmul2  20030  ringnegl  20205  ringnegr  20206  ringmneg2  20208  rdivmuldivd  20316  imadrhmcl  20700  lmodfopne  20821  lmodvsneg  20827  lssvs0or  21035  lvecinv  21038  lspabs2  21045  zringunit  21391  zringcyg  21394  dvdschrmulg  21453  fermltlchr  21454  sraassab  21793  mplcoe3  21961  mplcoe5  21963  evlvar  22023  psd1  22070  mdetrlin  22505  mdetunilem6  22520  cramerimplem3  22588  cramerimp  22589  paste  23197  tuslem  24170  tususs  24173  ngpds  24508  ioo2bl  24697  ipcau2  25150  dvexp3  25898  rolle  25910  cmvth  25911  cmvthOLD  25912  dv11cn  25922  lhop  25937  itgsubstlem  25971  itgpowd  25973  ply1divex  26058  fta1glem1  26089  fta1g  26091  dgrnznn  26168  fta1  26232  vieta1lem2  26235  aaliou2  26264  dvtaylp  26294  dvntaylp  26295  taylthlem1  26297  taylthlem2  26298  taylthlem2OLD  26299  dvradcnv  26346  ptolemy  26421  coskpi  26448  tanregt0  26464  cxpeq  26683  isosctrlem2  26745  chordthmlem  26758  dcubic  26772  quart1lem  26781  tanatan  26845  atantan  26849  dvatan  26861  birthdaylem2  26878  rlimcxp  26900  jensenlem2  26914  logdiflbnd  26921  emcllem2  26923  lgamgulmlem2  26956  lgamcvg2  26981  basellem8  27014  bclbnd  27207  lgsqr  27278  lgseisenlem3  27304  lgseisenlem4  27305  lgsquadlem1  27307  lgsquadlem2  27308  rpvmasumlem  27414  dchrisumlem1  27416  dchrisum0flblem1  27435  dchrisum0flblem2  27436  dchrisum0re  27440  dchrisum0lem1  27443  mudivsum  27457  mulogsum  27459  vmalogdivsum2  27465  logsqvma2  27470  selberg2lem  27477  logdivbnd  27483  selbergr  27495  selberg3r  27496  pntrlog2bndlem4  27507  pntrlog2bndlem5  27508  pntpbnd2  27514  pw2divscan4d  28354  pw2cutp1  28367  zs12zodd  28377  miduniq  28648  krippenlem  28653  colperpexlem2  28694  ttgcontlem1  28848  brbtwn2  28868  colinearalglem4  28872  axsegconlem9  28888  ax5seglem1  28891  axbtwnid  28902  axeuclidlem  28925  axcontlem2  28928  axcontlem4  28930  grpoinvid1  30490  vcz  30537  hosubsub4  31780  lnop0  31928  branmfn  32067  fressupp  32644  difico  32739  wrdsplex  32890  s3f1  32901  ccatf1  32903  mgcf1o  32958  mndlrinv  32991  cycpmco2lem4  33084  tocyccntz  33099  cyc3genpm  33107  cycpmconjslem2  33110  kerunit  33276  qustrivr  33315  znfermltl  33316  linds2eq  33331  dvdsruassoi  33334  dvdsruasso  33335  qsdrnglem2  33446  zringfrac  33504  m1pmeq  33531  vr1nz  33538  ply1degltdimlem  33597  fedgmullem2  33605  fldextrspunlsplem  33647  constrrtll  33700  constrrtlc1  33701  constrrtcclem  33703  constrrtcc  33704  constrrecl  33738  2sqr3minply  33749  cos9thpiminplylem1  33751  cos9thpiminplylem2  33752  carsggect  34288  carsgclctunlem2  34289  ballotlemfrceq  34499  ballotlemrinv0  34503  hashreprin  34590  hgt750lemb  34626  faclimlem1  35718  irrdifflemf  37301  poimirlem4  37606  poimirlem23  37625  mblfinlem2  37640  voliunnfl  37646  volsupnfl  37647  itg2addnclem3  37655  ftc2nc  37684  dvasin  37686  areacirclem1  37690  areacirclem4  37693  rngonegmn1l  37923  rngonegmn1r  37924  lfl0  39046  latmassOLD  39210  omlmod1i2N  39241  llnexchb2lem  39850  dalawlem3  39855  pmapj2N  39911  osumcllem9N  39946  pexmidlem6N  39957  4atexlemc  40051  cdleme1  40209  cdleme42a  40453  cdlemg13a  40633  cdlemh2  40798  cdlemk1  40813  tendocnv  41003  dihmeetlem12N  41300  dihmeetlem16N  41304  dihmeetlem19N  41307  dochsatshp  41433  dochexmidlem6  41447  mapdval4N  41614  mapdpglem28  41683  mapdpglem31  41685  mapdindp4  41705  hdmap14lem1a  41848  hdmapinvlem4  41903  3rdpwhole  42268  oexpreposd  42298  remul01  42383  sn-negex12  42393  sn-subeu  42403  remulinvcom  42409  sn-0tie0  42427  cnreeu  42466  fltnlta  42639  irrapxlem5  42802  pellfund14  42874  rmxdbl  42915  jm2.22  42971  oaabsb  43270  oaun2  43357  oaun3  43358  sqrtcval  43617  0ellimcdiv  45634  fourierdlem95  46186  etransclem46  46265  sigariz  46848  ichreuopeq  47461  gricushgr  47905  altgsumbc  48340  blengt1fldiv2p1  48582  restclsseplem  48903  cofu1a  49083  cofu2a  49084  uobeqw  49208  swapf2fval  49254  swapf1val  49256  coccom  49653