Theorem 3eqtr3rd 2783

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

Syntax hints:   → wi 4   = wceq 1536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726

This theorem is referenced by:  iunxdif3  5099  fcofo  7307  fcof1oinvd  7312  cantnfp1lem3  9717  fin1a2lem7  10443  prlem934  11070  addlid  11441  addcom  11444  addcomd  11460  negeu  11495  add20  11772  2halves  12491  bcnn  14347  bcpasc  14356  hashfun  14472  hashf1dmrn  14478  wrdeqs1cat  14754  sqreulem  15394  summolem3  15746  fsumneg  15819  geolim  15902  geolim2  15903  mertens  15918  prodmolem3  15965  fallrisefac  16057  bpoly3  16090  sincossq  16208  demoivre  16232  eirrlem  16236  oddpwp1fsum  16425  sadeq  16505  gcdid  16560  gcdmultipled  16567  nn0rppwr  16594  phiprmpw  16809  pythagtriplem12  16859  expnprm  16935  fullresc  17901  grpinvid1  19021  grpnpcan  19062  grplactcnv  19073  ghmgrp  19096  conjghm  19279  odmodnn0  19572  gex1  19623  sylow3lem3  19661  efgredeu  19784  odadd2  19881  gsumval3  19939  pgpfac1lem3a  20110  ringnegl  20315  ringnegr  20316  ringmneg2  20318  rdivmuldivd  20429  imadrhmcl  20814  lmodfopne  20914  lmodvsneg  20920  lssvs0or  21129  lvecinv  21132  lspabs2  21139  zringunit  21494  zringcyg  21497  dvdschrmulg  21560  fermltlchr  21561  sraassab  21905  mplcoe3  22073  mplcoe5  22075  evlvar  22141  psd1  22188  mdetrlin  22623  mdetunilem6  22638  cramerimplem3  22706  cramerimp  22707  paste  23317  tuslem  24290  tuslemOLD  24291  tususs  24294  ngpds  24632  ioo2bl  24828  ipcau2  25281  dvexp3  26030  rolle  26042  cmvth  26043  cmvthOLD  26044  dv11cn  26054  lhop  26069  itgsubstlem  26103  itgpowd  26105  ply1divex  26190  fta1glem1  26221  fta1g  26223  dgrnznn  26300  fta1  26364  vieta1lem2  26367  aaliou2  26396  dvtaylp  26426  dvntaylp  26427  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  dvradcnv  26478  ptolemy  26552  coskpi  26579  tanregt0  26595  cxpeq  26814  isosctrlem2  26876  chordthmlem  26889  dcubic  26903  quart1lem  26912  tanatan  26976  atantan  26980  dvatan  26992  birthdaylem2  27009  rlimcxp  27031  jensenlem2  27045  logdiflbnd  27052  emcllem2  27054  lgamgulmlem2  27087  lgamcvg2  27112  basellem8  27145  bclbnd  27338  lgsqr  27409  lgseisenlem3  27435  lgseisenlem4  27436  lgsquadlem1  27438  lgsquadlem2  27439  rpvmasumlem  27545  dchrisumlem1  27547  dchrisum0flblem1  27566  dchrisum0flblem2  27567  dchrisum0re  27571  dchrisum0lem1  27574  mudivsum  27588  mulogsum  27590  vmalogdivsum2  27596  logsqvma2  27601  selberg2lem  27608  logdivbnd  27614  selbergr  27626  selberg3r  27627  pntrlog2bndlem4  27638  pntrlog2bndlem5  27639  pntpbnd2  27645  miduniq  28707  krippenlem  28712  colperpexlem2  28753  ttgcontlem1  28913  brbtwn2  28934  colinearalglem4  28938  axsegconlem9  28954  ax5seglem1  28957  axbtwnid  28968  axeuclidlem  28991  axcontlem2  28994  axcontlem4  28996  grpoinvid1  30556  vcz  30603  hosubsub4  31846  lnop0  31994  branmfn  32133  fressupp  32702  difico  32791  wrdsplex  32904  s3f1  32915  ccatf1  32917  mgcf1o  32977  mndlrinv  33011  omndmul2  33071  cycpmco2lem4  33131  tocyccntz  33146  cyc3genpm  33154  cycpmconjslem2  33157  kerunit  33328  qustrivr  33372  znfermltl  33373  linds2eq  33388  dvdsruassoi  33391  dvdsruasso  33392  qsdrnglem2  33503  zringfrac  33561  m1pmeq  33587  ply1degltdimlem  33649  fedgmullem2  33657  constrrtll  33736  constrrtlc1  33737  constrrtcclem  33739  constrrtcc  33740  2sqr3minply  33752  carsggect  34299  carsgclctunlem2  34300  ballotlemfrceq  34509  ballotlemrinv0  34513  hashreprin  34613  hgt750lemb  34649  faclimlem1  35722  irrdifflemf  37307  poimirlem4  37610  poimirlem23  37629  mblfinlem2  37644  voliunnfl  37650  volsupnfl  37651  itg2addnclem3  37659  ftc2nc  37688  dvasin  37690  areacirclem1  37694  areacirclem4  37697  rngonegmn1l  37927  rngonegmn1r  37928  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  oexpreposd  42335  sn-00idlem3  42406  remul01  42413  sn-negex12  42422  sn-subeu  42432  remulinvcom  42438  sn-0tie0  42445  cnreeu  42476  fltnlta  42649  irrapxlem5  42813  pellfund14  42885  rmxdbl  42927  jm2.22  42983  oaabsb  43283  oaun2  43370  oaun3  43371  sqrtcval  43630  0ellimcdiv  45604  fourierdlem95  46156  etransclem46  46235  sigariz  46818  ichreuopeq  47397  gricushgr  47823  altgsumbc  48196  blengt1fldiv2p1  48442  restclsseplem  48710