Theorem 3eqtr3rd 2787

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 2780	. 2 ⊢ (𝜑 → 𝐵 = 𝐶)
5	1, 4	eqtr3d 2780	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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1784  df-cleq 2730

This theorem is referenced by:  iunxdif3  5020  fcofo  7140  fcof1oinvd  7145  cantnfp1lem3  9368  fin1a2lem7  10093  prlem934  10720  addid2  11088  addcom  11091  addcomd  11107  negeu  11141  add20  11417  2halves  12131  bcnn  13954  bcpasc  13963  hashfun  14080  wrdeqs1cat  14361  sqreulem  14999  summolem3  15354  fsumneg  15427  geolim  15510  geolim2  15511  mertens  15526  prodmolem3  15571  fallrisefac  15663  bpoly3  15696  sincossq  15813  demoivre  15837  eirrlem  15841  oddpwp1fsum  16029  sadeq  16107  gcdid  16162  gcdmultipled  16170  phiprmpw  16405  pythagtriplem12  16455  expnprm  16531  fullresc  17482  grpinvid1  18545  grpnpcan  18582  grplactcnv  18593  ghmgrp  18614  conjghm  18780  odmodnn0  19063  gex1  19111  sylow3lem3  19149  efgredeu  19273  odadd2  19365  gsumval3  19423  pgpfac1lem3a  19594  ringnegl  19748  rngnegr  19749  ringmneg2  19751  lmodfopne  20076  lmodvsneg  20082  lss0v  20193  lssvs0or  20287  lvecinv  20290  lspabs2  20297  zringunit  20600  zringcyg  20603  mplcoe3  21149  mplcoe5  21151  evlvar  21220  mdetrlin  21659  mdetunilem6  21674  cramerimplem3  21742  cramerimp  21743  paste  22353  tuslem  23326  tuslemOLD  23327  tususs  23330  ngpds  23666  ioo2bl  23862  ipcau2  24303  dvexp3  25047  rolle  25059  cmvth  25060  dv11cn  25070  lhop  25085  itgsubstlem  25117  itgpowd  25119  ply1divex  25206  fta1glem1  25235  fta1g  25237  dgrnznn  25313  fta1  25373  vieta1lem2  25376  aaliou2  25405  dvtaylp  25434  dvntaylp  25435  taylthlem1  25437  taylthlem2  25438  dvradcnv  25485  ptolemy  25558  coskpi  25584  tanregt0  25600  cxpeq  25815  isosctrlem2  25874  chordthmlem  25887  dcubic  25901  quart1lem  25910  tanatan  25974  atantan  25978  dvatan  25990  birthdaylem2  26007  rlimcxp  26028  jensenlem2  26042  logdiflbnd  26049  emcllem2  26051  lgamgulmlem2  26084  lgamcvg2  26109  basellem8  26142  bclbnd  26333  lgsqr  26404  lgseisenlem3  26430  lgseisenlem4  26431  lgsquadlem1  26433  lgsquadlem2  26434  rpvmasumlem  26540  dchrisumlem1  26542  dchrisum0flblem1  26561  dchrisum0flblem2  26562  dchrisum0re  26566  dchrisum0lem1  26569  mudivsum  26583  mulogsum  26585  vmalogdivsum2  26591  logsqvma2  26596  selberg2lem  26603  logdivbnd  26609  selbergr  26621  selberg3r  26622  pntrlog2bndlem4  26633  pntrlog2bndlem5  26634  pntpbnd2  26640  miduniq  26950  krippenlem  26955  colperpexlem2  26996  ttgcontlem1  27155  brbtwn2  27176  colinearalglem4  27180  axsegconlem9  27196  ax5seglem1  27199  axbtwnid  27210  axeuclidlem  27233  axcontlem2  27236  axcontlem4  27238  grpoinvid1  28791  vcz  28838  hosubsub4  30081  lnop0  30229  branmfn  30368  fressupp  30924  difico  31006  wrdsplex  31114  s3f1  31123  ccatf1  31125  mgcf1o  31183  omndmul2  31240  cycpmco2lem4  31298  tocyccntz  31313  cyc3genpm  31321  cycpmconjslem2  31324  dvdschrmulg  31385  rdivmuldivd  31390  kerunit  31424  qustrivr  31463  znfermltl  31464  linds2eq  31477  fedgmullem2  31613  carsggect  32185  carsgclctunlem2  32186  ballotlemfrceq  32395  ballotlemrinv0  32399  hashreprin  32500  hgt750lemb  32536  hashf1dmrn  32975  faclimlem1  33615  irrdifflemf  35423  poimirlem4  35708  poimirlem23  35727  mblfinlem2  35742  voliunnfl  35748  volsupnfl  35749  itg2addnclem3  35757  ftc2nc  35786  dvasin  35788  areacirclem1  35792  areacirclem4  35795  rngonegmn1l  36026  rngonegmn1r  36027  lfl0  37006  latmassOLD  37170  omlmod1i2N  37201  llnexchb2lem  37809  dalawlem3  37814  pmapj2N  37870  osumcllem9N  37905  pexmidlem6N  37916  4atexlemc  38010  cdleme1  38168  cdleme42a  38412  cdlemg13a  38592  cdlemh2  38757  cdlemk1  38772  tendocnv  38962  dihmeetlem12N  39259  dihmeetlem16N  39263  dihmeetlem19N  39266  dochsatshp  39392  dochexmidlem6  39406  mapdval4N  39573  mapdpglem28  39642  mapdpglem31  39644  mapdindp4  39664  hdmap14lem1a  39807  hdmapinvlem4  39862  oexpreposd  40242  nn0rppwr  40254  sn-00idlem3  40304  remul01  40311  sn-subeu  40329  remulinvcom  40335  sn-0tie0  40342  cnreeu  40359  fltnlta  40416  irrapxlem5  40564  pellfund14  40636  rmxdbl  40677  jm2.22  40733  sqrtcval  41138  0ellimcdiv  43080  fourierdlem95  43632  etransclem46  43711  sigariz  44266  ichreuopeq  44813  isomushgr  45166  altgsumbc  45576  blengt1fldiv2p1  45827  restclsseplem  46096