Theorem 3eqtr3rd 2779

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 2772	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2772	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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  iunxdif3  5071  fcofo  7281  fcof1oinvd  7286  cantnfp1lem3  9694  fin1a2lem7  10420  prlem934  11047  addlid  11418  addcom  11421  addcomd  11437  negeu  11472  add20  11749  2halves  12459  bcnn  14330  bcpasc  14339  hashfun  14455  hashf1dmrn  14461  wrdeqs1cat  14738  sqreulem  15378  summolem3  15730  fsumneg  15803  geolim  15886  geolim2  15887  mertens  15902  prodmolem3  15949  fallrisefac  16041  bpoly3  16074  sincossq  16194  demoivre  16218  eirrlem  16222  oddpwp1fsum  16411  sadeq  16491  gcdid  16546  gcdmultipled  16553  nn0rppwr  16580  phiprmpw  16795  pythagtriplem12  16846  expnprm  16922  fullresc  17864  grpinvid1  18974  grpnpcan  19015  grplactcnv  19026  ghmgrp  19049  conjghm  19232  odmodnn0  19521  gex1  19572  sylow3lem3  19610  efgredeu  19733  odadd2  19830  gsumval3  19888  pgpfac1lem3a  20059  ringnegl  20262  ringnegr  20263  ringmneg2  20265  rdivmuldivd  20373  imadrhmcl  20757  lmodfopne  20857  lmodvsneg  20863  lssvs0or  21071  lvecinv  21074  lspabs2  21081  zringunit  21427  zringcyg  21430  dvdschrmulg  21489  fermltlchr  21490  sraassab  21828  mplcoe3  21996  mplcoe5  21998  evlvar  22058  psd1  22105  mdetrlin  22540  mdetunilem6  22555  cramerimplem3  22623  cramerimp  22624  paste  23232  tuslem  24205  tususs  24208  ngpds  24543  ioo2bl  24732  ipcau2  25186  dvexp3  25934  rolle  25946  cmvth  25947  cmvthOLD  25948  dv11cn  25958  lhop  25973  itgsubstlem  26007  itgpowd  26009  ply1divex  26094  fta1glem1  26125  fta1g  26127  dgrnznn  26204  fta1  26268  vieta1lem2  26271  aaliou2  26300  dvtaylp  26330  dvntaylp  26331  taylthlem1  26333  taylthlem2  26334  taylthlem2OLD  26335  dvradcnv  26382  ptolemy  26457  coskpi  26484  tanregt0  26500  cxpeq  26719  isosctrlem2  26781  chordthmlem  26794  dcubic  26808  quart1lem  26817  tanatan  26881  atantan  26885  dvatan  26897  birthdaylem2  26914  rlimcxp  26936  jensenlem2  26950  logdiflbnd  26957  emcllem2  26959  lgamgulmlem2  26992  lgamcvg2  27017  basellem8  27050  bclbnd  27243  lgsqr  27314  lgseisenlem3  27340  lgseisenlem4  27341  lgsquadlem1  27343  lgsquadlem2  27344  rpvmasumlem  27450  dchrisumlem1  27452  dchrisum0flblem1  27471  dchrisum0flblem2  27472  dchrisum0re  27476  dchrisum0lem1  27479  mudivsum  27493  mulogsum  27495  vmalogdivsum2  27501  logsqvma2  27506  selberg2lem  27513  logdivbnd  27519  selbergr  27531  selberg3r  27532  pntrlog2bndlem4  27543  pntrlog2bndlem5  27544  pntpbnd2  27550  pw2cutp1  28388  miduniq  28664  krippenlem  28669  colperpexlem2  28710  ttgcontlem1  28864  brbtwn2  28884  colinearalglem4  28888  axsegconlem9  28904  ax5seglem1  28907  axbtwnid  28918  axeuclidlem  28941  axcontlem2  28944  axcontlem4  28946  grpoinvid1  30509  vcz  30556  hosubsub4  31799  lnop0  31947  branmfn  32086  fressupp  32665  difico  32760  wrdsplex  32911  s3f1  32922  ccatf1  32924  mgcf1o  32983  mndlrinv  33019  omndmul2  33080  cycpmco2lem4  33140  tocyccntz  33155  cyc3genpm  33163  cycpmconjslem2  33166  kerunit  33341  qustrivr  33380  znfermltl  33381  linds2eq  33396  dvdsruassoi  33399  dvdsruasso  33400  qsdrnglem2  33511  zringfrac  33569  m1pmeq  33596  vr1nz  33603  ply1degltdimlem  33662  fedgmullem2  33670  fldextrspunlsplem  33714  constrrtll  33765  constrrtlc1  33766  constrrtcclem  33768  constrrtcc  33769  constrrecl  33803  2sqr3minply  33814  cos9thpiminplylem1  33816  cos9thpiminplylem2  33817  carsggect  34350  carsgclctunlem2  34351  ballotlemfrceq  34561  ballotlemrinv0  34565  hashreprin  34652  hgt750lemb  34688  faclimlem1  35760  irrdifflemf  37343  poimirlem4  37648  poimirlem23  37667  mblfinlem2  37682  voliunnfl  37688  volsupnfl  37689  itg2addnclem3  37697  ftc2nc  37726  dvasin  37728  areacirclem1  37732  areacirclem4  37735  rngonegmn1l  37965  rngonegmn1r  37966  lfl0  39083  latmassOLD  39247  omlmod1i2N  39278  llnexchb2lem  39887  dalawlem3  39892  pmapj2N  39948  osumcllem9N  39983  pexmidlem6N  39994  4atexlemc  40088  cdleme1  40246  cdleme42a  40490  cdlemg13a  40670  cdlemh2  40835  cdlemk1  40850  tendocnv  41040  dihmeetlem12N  41337  dihmeetlem16N  41341  dihmeetlem19N  41344  dochsatshp  41470  dochexmidlem6  41484  mapdval4N  41651  mapdpglem28  41720  mapdpglem31  41722  mapdindp4  41742  hdmap14lem1a  41885  hdmapinvlem4  41940  oexpreposd  42371  sn-00idlem3  42443  remul01  42450  sn-negex12  42459  sn-subeu  42469  remulinvcom  42475  sn-0tie0  42482  cnreeu  42513  fltnlta  42686  irrapxlem5  42849  pellfund14  42921  rmxdbl  42963  jm2.22  43019  oaabsb  43318  oaun2  43405  oaun3  43406  sqrtcval  43665  0ellimcdiv  45678  fourierdlem95  46230  etransclem46  46309  sigariz  46892  ichreuopeq  47487  gricushgr  47930  altgsumbc  48327  blengt1fldiv2p1  48573  restclsseplem  48889  swapf2fval  49182  swapf1val  49184  coccom  49534