Theorem 3eqtr3rd 2788

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

Syntax hints:   → wi 4   = wceq 1539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731

This theorem is referenced by:  iunxdif3  5025  fcofo  7169  fcof1oinvd  7174  cantnfp1lem3  9447  fin1a2lem7  10171  prlem934  10798  addid2  11167  addcom  11170  addcomd  11186  negeu  11220  add20  11496  2halves  12210  bcnn  14035  bcpasc  14044  hashfun  14161  wrdeqs1cat  14442  sqreulem  15080  summolem3  15435  fsumneg  15508  geolim  15591  geolim2  15592  mertens  15607  prodmolem3  15652  fallrisefac  15744  bpoly3  15777  sincossq  15894  demoivre  15918  eirrlem  15922  oddpwp1fsum  16110  sadeq  16188  gcdid  16243  gcdmultipled  16251  phiprmpw  16486  pythagtriplem12  16536  expnprm  16612  fullresc  17575  grpinvid1  18639  grpnpcan  18676  grplactcnv  18687  ghmgrp  18708  conjghm  18874  odmodnn0  19157  gex1  19205  sylow3lem3  19243  efgredeu  19367  odadd2  19459  gsumval3  19517  pgpfac1lem3a  19688  ringnegl  19842  rngnegr  19843  ringmneg2  19845  lmodfopne  20170  lmodvsneg  20176  lss0v  20287  lssvs0or  20381  lvecinv  20384  lspabs2  20391  zringunit  20697  zringcyg  20700  mplcoe3  21248  mplcoe5  21250  evlvar  21319  mdetrlin  21760  mdetunilem6  21775  cramerimplem3  21843  cramerimp  21844  paste  22454  tuslem  23427  tuslemOLD  23428  tususs  23431  ngpds  23769  ioo2bl  23965  ipcau2  24407  dvexp3  25151  rolle  25163  cmvth  25164  dv11cn  25174  lhop  25189  itgsubstlem  25221  itgpowd  25223  ply1divex  25310  fta1glem1  25339  fta1g  25341  dgrnznn  25417  fta1  25477  vieta1lem2  25480  aaliou2  25509  dvtaylp  25538  dvntaylp  25539  taylthlem1  25541  taylthlem2  25542  dvradcnv  25589  ptolemy  25662  coskpi  25688  tanregt0  25704  cxpeq  25919  isosctrlem2  25978  chordthmlem  25991  dcubic  26005  quart1lem  26014  tanatan  26078  atantan  26082  dvatan  26094  birthdaylem2  26111  rlimcxp  26132  jensenlem2  26146  logdiflbnd  26153  emcllem2  26155  lgamgulmlem2  26188  lgamcvg2  26213  basellem8  26246  bclbnd  26437  lgsqr  26508  lgseisenlem3  26534  lgseisenlem4  26535  lgsquadlem1  26537  lgsquadlem2  26538  rpvmasumlem  26644  dchrisumlem1  26646  dchrisum0flblem1  26665  dchrisum0flblem2  26666  dchrisum0re  26670  dchrisum0lem1  26673  mudivsum  26687  mulogsum  26689  vmalogdivsum2  26695  logsqvma2  26700  selberg2lem  26707  logdivbnd  26713  selbergr  26725  selberg3r  26726  pntrlog2bndlem4  26737  pntrlog2bndlem5  26738  pntpbnd2  26744  miduniq  27055  krippenlem  27060  colperpexlem2  27101  ttgcontlem1  27261  brbtwn2  27282  colinearalglem4  27286  axsegconlem9  27302  ax5seglem1  27305  axbtwnid  27316  axeuclidlem  27339  axcontlem2  27342  axcontlem4  27344  grpoinvid1  28899  vcz  28946  hosubsub4  30189  lnop0  30337  branmfn  30476  fressupp  31031  difico  31113  wrdsplex  31221  s3f1  31230  ccatf1  31232  mgcf1o  31290  omndmul2  31347  cycpmco2lem4  31405  tocyccntz  31420  cyc3genpm  31428  cycpmconjslem2  31431  dvdschrmulg  31492  rdivmuldivd  31497  kerunit  31531  qustrivr  31570  znfermltl  31571  linds2eq  31584  fedgmullem2  31720  carsggect  32294  carsgclctunlem2  32295  ballotlemfrceq  32504  ballotlemrinv0  32508  hashreprin  32609  hgt750lemb  32645  hashf1dmrn  33084  faclimlem1  33718  irrdifflemf  35505  poimirlem4  35790  poimirlem23  35809  mblfinlem2  35824  voliunnfl  35830  volsupnfl  35831  itg2addnclem3  35839  ftc2nc  35868  dvasin  35870  areacirclem1  35874  areacirclem4  35877  rngonegmn1l  36108  rngonegmn1r  36109  lfl0  37086  latmassOLD  37250  omlmod1i2N  37281  llnexchb2lem  37889  dalawlem3  37894  pmapj2N  37950  osumcllem9N  37985  pexmidlem6N  37996  4atexlemc  38090  cdleme1  38248  cdleme42a  38492  cdlemg13a  38672  cdlemh2  38837  cdlemk1  38852  tendocnv  39042  dihmeetlem12N  39339  dihmeetlem16N  39343  dihmeetlem19N  39346  dochsatshp  39472  dochexmidlem6  39486  mapdval4N  39653  mapdpglem28  39722  mapdpglem31  39724  mapdindp4  39744  hdmap14lem1a  39887  hdmapinvlem4  39942  oexpreposd  40328  nn0rppwr  40340  sn-00idlem3  40390  remul01  40397  sn-subeu  40415  remulinvcom  40421  sn-0tie0  40428  cnreeu  40445  fltnlta  40507  irrapxlem5  40655  pellfund14  40727  rmxdbl  40768  jm2.22  40824  sqrtcval  41256  0ellimcdiv  43197  fourierdlem95  43749  etransclem46  43828  sigariz  44390  ichreuopeq  44936  isomushgr  45289  altgsumbc  45699  blengt1fldiv2p1  45950  restclsseplem  46219