Theorem 3eqtr3rd 2653

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

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  iunxdif3  4542  fcofo  6443  fcof1oinvd  6448  cantnfp1lem3  8460  fin1a2lem7  9111  prlem934  9734  addid2  10098  addcom  10101  addcomd  10117  negeu  10150  add20  10419  2halves  11137  bcnn  12961  bcpasc  12970  hashfun  13084  wrdeqs1cat  13326  sqreulem  13947  summolem3  14292  fsumneg  14361  geolim  14440  geolim2  14441  mertens  14457  prodmolem3  14502  fallrisefac  14595  bpoly3  14628  sincossq  14745  demoivre  14769  eirrlem  14771  oddpwp1fsum  14953  sadeq  15032  gcdid  15086  phiprmpw  15319  pythagtriplem12  15369  expnprm  15444  fullresc  16334  grpinvid1  17293  grpnpcan  17330  grplactcnv  17341  ghmgrp  17362  conjghm  17514  odmodnn0  17782  gex1  17829  sylow3lem3  17867  efgredeu  17988  odadd2  18075  gsumval3  18131  pgpfac1lem3a  18298  ringnegl  18417  rngnegr  18418  ringmneg2  18420  lmodfopne  18724  lmodvsneg  18730  lss0v  18837  lssvs0or  18931  lvecinv  18934  lspabs2  18941  mplcoe3  19287  mplcoe5  19289  evlvar  19350  zringunit  19655  zringcyg  19658  mdetrlin  20227  mdetunilem6  20242  cramerimplem3  20310  cramerimp  20311  paste  20908  tuslem  21881  tususs  21884  ngpds  22218  ioo2bl  22404  ipcau2  22841  dvexp3  23545  rolle  23557  cmvth  23558  dv11cn  23568  lhop  23583  itgsubstlem  23615  ply1divex  23700  fta1glem1  23729  fta1g  23731  dgrnznn  23807  fta1  23867  vieta1lem2  23870  aaliou2  23899  dvtaylp  23928  dvntaylp  23929  taylthlem1  23931  taylthlem2  23932  dvradcnv  23979  ptolemy  24052  coskpi  24076  tanregt0  24089  cxpeq  24298  isosctrlem2  24349  chordthmlem  24359  dcubic  24373  quart1lem  24382  tanatan  24446  atantan  24450  dvatan  24462  birthdaylem2  24479  rlimcxp  24500  jensenlem2  24514  logdiflbnd  24521  emcllem2  24523  lgamgulmlem2  24556  lgamcvg2  24581  basellem8  24614  bclbnd  24805  lgsqr  24876  lgseisenlem3  24902  lgseisenlem4  24903  lgsquadlem1  24905  lgsquadlem2  24906  rpvmasumlem  24976  dchrisumlem1  24978  dchrisum0flblem1  24997  dchrisum0flblem2  24998  dchrisum0re  25002  dchrisum0lem1  25005  mudivsum  25019  mulogsum  25021  vmalogdivsum2  25027  logsqvma2  25032  selberg2lem  25039  logdivbnd  25045  selbergr  25057  selberg3r  25058  pntrlog2bndlem4  25069  pntrlog2bndlem5  25070  pntpbnd2  25076  miduniq  25380  krippenlem  25385  colperpexlem2  25423  ttgcontlem1  25565  brbtwn2  25585  colinearalglem4  25589  axsegconlem9  25605  ax5seglem1  25608  axbtwnid  25619  axeuclidlem  25642  axcontlem2  25645  axcontlem4  25647  clwwlkel  26321  grpoinvid1  26766  vcz  26814  hosubsub4  28061  lnop0  28209  branmfn  28348  difico  28935  omndmul2  29043  rdivmuldivd  29122  kerunit  29154  carsggect  29707  carsgclctunlem2  29708  ballotlemfrceq  29917  ballotlemrinv0  29921  wrdsplex  29944  faclimlem1  30882  poimirlem4  32583  poimirlem23  32602  mblfinlem2  32617  voliunnfl  32623  volsupnfl  32624  itg2addnclem3  32633  ftc2nc  32664  dvasin  32666  areacirclem1  32670  areacirclem4  32673  rngonegmn1l  32910  rngonegmn1r  32911  lfl0  33370  latmassOLD  33534  omlmod1i2N  33565  llnexchb2lem  34172  dalawlem3  34177  pmapj2N  34233  osumcllem9N  34268  pexmidlem6N  34279  4atexlemc  34373  cdleme1  34532  cdleme42a  34777  cdlemg13a  34957  cdlemh2  35122  cdlemk1  35137  tendocnv  35328  dihmeetlem12N  35625  dihmeetlem16N  35629  dihmeetlem19N  35632  dochsatshp  35758  dochexmidlem6  35772  mapdval4N  35939  mapdpglem28  36008  mapdpglem31  36010  mapdindp4  36030  hdmap14lem1a  36176  hdmapinvlem4  36231  irrapxlem5  36408  pellfund14  36480  rmxdbl  36522  jm2.22  36580  itgpowd  36819  0ellimcdiv  38716  fourierdlem95  39094  etransclem46  39173  sigariz  39701  clwwlksel  41221  altgsumbc  41923  blengt1fldiv2p1  42185