Theorem 3eqtr3rd 2789

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732

This theorem is referenced by:  iunxdif3  5118  fcofo  7324  fcof1oinvd  7329  cantnfp1lem3  9749  fin1a2lem7  10475  prlem934  11102  addlid  11473  addcom  11476  addcomd  11492  negeu  11526  add20  11802  2halves  12521  bcnn  14361  bcpasc  14370  hashfun  14486  hashf1dmrn  14492  wrdeqs1cat  14768  sqreulem  15408  summolem3  15762  fsumneg  15835  geolim  15918  geolim2  15919  mertens  15934  prodmolem3  15981  fallrisefac  16073  bpoly3  16106  sincossq  16224  demoivre  16248  eirrlem  16252  oddpwp1fsum  16440  sadeq  16518  gcdid  16573  gcdmultipled  16581  nn0rppwr  16608  phiprmpw  16823  pythagtriplem12  16873  expnprm  16949  fullresc  17915  grpinvid1  19031  grpnpcan  19072  grplactcnv  19083  ghmgrp  19106  conjghm  19289  odmodnn0  19582  gex1  19633  sylow3lem3  19671  efgredeu  19794  odadd2  19891  gsumval3  19949  pgpfac1lem3a  20120  ringnegl  20325  ringnegr  20326  ringmneg2  20328  rdivmuldivd  20439  imadrhmcl  20820  lmodfopne  20920  lmodvsneg  20926  lssvs0or  21135  lvecinv  21138  lspabs2  21145  zringunit  21500  zringcyg  21503  dvdschrmulg  21566  fermltlchr  21567  sraassab  21911  mplcoe3  22079  mplcoe5  22081  evlvar  22147  psd1  22194  mdetrlin  22629  mdetunilem6  22644  cramerimplem3  22712  cramerimp  22713  paste  23323  tuslem  24296  tuslemOLD  24297  tususs  24300  ngpds  24638  ioo2bl  24834  ipcau2  25287  dvexp3  26036  rolle  26048  cmvth  26049  cmvthOLD  26050  dv11cn  26060  lhop  26075  itgsubstlem  26109  itgpowd  26111  ply1divex  26196  fta1glem1  26227  fta1g  26229  dgrnznn  26306  fta1  26368  vieta1lem2  26371  aaliou2  26400  dvtaylp  26430  dvntaylp  26431  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  dvradcnv  26482  ptolemy  26556  coskpi  26583  tanregt0  26599  cxpeq  26818  isosctrlem2  26880  chordthmlem  26893  dcubic  26907  quart1lem  26916  tanatan  26980  atantan  26984  dvatan  26996  birthdaylem2  27013  rlimcxp  27035  jensenlem2  27049  logdiflbnd  27056  emcllem2  27058  lgamgulmlem2  27091  lgamcvg2  27116  basellem8  27149  bclbnd  27342  lgsqr  27413  lgseisenlem3  27439  lgseisenlem4  27440  lgsquadlem1  27442  lgsquadlem2  27443  rpvmasumlem  27549  dchrisumlem1  27551  dchrisum0flblem1  27570  dchrisum0flblem2  27571  dchrisum0re  27575  dchrisum0lem1  27578  mudivsum  27592  mulogsum  27594  vmalogdivsum2  27600  logsqvma2  27605  selberg2lem  27612  logdivbnd  27618  selbergr  27630  selberg3r  27631  pntrlog2bndlem4  27642  pntrlog2bndlem5  27643  pntpbnd2  27649  miduniq  28711  krippenlem  28716  colperpexlem2  28757  ttgcontlem1  28917  brbtwn2  28938  colinearalglem4  28942  axsegconlem9  28958  ax5seglem1  28961  axbtwnid  28972  axeuclidlem  28995  axcontlem2  28998  axcontlem4  29000  grpoinvid1  30560  vcz  30607  hosubsub4  31850  lnop0  31998  branmfn  32137  fressupp  32700  difico  32788  wrdsplex  32902  s3f1  32913  ccatf1  32915  mgcf1o  32976  mndlrinv  33010  omndmul2  33062  cycpmco2lem4  33122  tocyccntz  33137  cyc3genpm  33145  cycpmconjslem2  33148  kerunit  33314  qustrivr  33358  znfermltl  33359  linds2eq  33374  dvdsruassoi  33377  dvdsruasso  33378  qsdrnglem2  33489  zringfrac  33547  m1pmeq  33573  ply1degltdimlem  33635  fedgmullem2  33643  constrrtll  33722  constrrtlc1  33723  constrrtcclem  33725  constrrtcc  33726  2sqr3minply  33738  carsggect  34283  carsgclctunlem2  34284  ballotlemfrceq  34493  ballotlemrinv0  34497  hashreprin  34597  hgt750lemb  34633  faclimlem1  35705  irrdifflemf  37291  poimirlem4  37584  poimirlem23  37603  mblfinlem2  37618  voliunnfl  37624  volsupnfl  37625  itg2addnclem3  37633  ftc2nc  37662  dvasin  37664  areacirclem1  37668  areacirclem4  37671  rngonegmn1l  37901  rngonegmn1r  37902  lfl0  39021  latmassOLD  39185  omlmod1i2N  39216  llnexchb2lem  39825  dalawlem3  39830  pmapj2N  39886  osumcllem9N  39921  pexmidlem6N  39932  4atexlemc  40026  cdleme1  40184  cdleme42a  40428  cdlemg13a  40608  cdlemh2  40773  cdlemk1  40788  tendocnv  40978  dihmeetlem12N  41275  dihmeetlem16N  41279  dihmeetlem19N  41282  dochsatshp  41408  dochexmidlem6  41422  mapdval4N  41589  mapdpglem28  41658  mapdpglem31  41660  mapdindp4  41680  hdmap14lem1a  41823  hdmapinvlem4  41878  oexpreposd  42309  sn-00idlem3  42376  remul01  42383  sn-negex12  42392  sn-subeu  42402  remulinvcom  42408  sn-0tie0  42415  cnreeu  42446  fltnlta  42618  irrapxlem5  42782  pellfund14  42854  rmxdbl  42896  jm2.22  42952  oaabsb  43256  oaun2  43343  oaun3  43344  sqrtcval  43603  0ellimcdiv  45570  fourierdlem95  46122  etransclem46  46201  sigariz  46784  ichreuopeq  47347  gricushgr  47770  altgsumbc  48077  blengt1fldiv2p1  48327  restclsseplem  48594