Theorem 3eqtr2rd 2778

Description: A deduction from three chained equalities. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3eqtr2d.1	⊢ (𝜑 → 𝐴 = 𝐵)
3eqtr2d.2	⊢ (𝜑 → 𝐶 = 𝐵)
3eqtr2d.3	⊢ (𝜑 → 𝐶 = 𝐷)

Assertion

Ref	Expression
3eqtr2rd	⊢ (𝜑 → 𝐷 = 𝐴)

Proof of Theorem 3eqtr2rd

Step	Hyp	Ref	Expression
1		3eqtr2d.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		3eqtr2d.2	. . 3 ⊢ (𝜑 → 𝐶 = 𝐵)
3	1, 2	eqtr4d 2774	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2772	1 ⊢ (𝜑 → 𝐷 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728

This theorem is referenced by:  nneob  8592  xp1d2m1eqxm1d2  12431  negmod  13878  modeqmodmin  13903  faclbnd2  14253  cats1un  14683  cjmulval  15107  fsumsplit  15703  fzosump1  15714  bcxmas  15800  trireciplem  15827  geo2sum  15838  geo2lim  15840  geoisum1c  15845  mertenslem1  15849  fprodsplit  15931  risefallfac  15989  bpolydiflem  16019  eftlub  16076  tanadd  16134  addsin  16137  subsin  16138  subcos  16142  sadadd2lem2  16419  qredeu  16627  zsqrtelqelz  16728  4sqlem15  16930  rcaninv  17761  resssetc  18059  resscatc  18076  curfcl  18198  mulgaddcomlem  19073  conjghm  19224  gasubg  19277  dfod2  19539  efginvrel2  19702  efgcpbllemb  19730  odadd2  19824  frgpnabllem1  19848  srgbinomlem3  20209  pws1  20304  prdslmodd  20964  znunithash  21544  frlmipval  21759  frlmlbs  21777  psrlmod  21938  restcld  23137  clmneg  25048  rrxds  25360  itg2monolem1  25717  itgconst  25786  dvexp  25920  dvfsumabs  25990  dvtaylp  26335  taylthlem2  26339  tangtx  26469  logsqrt  26668  zrtelqelz  26722  lawcoslem1  26779  chordthmlem2  26797  chordthmlem4  26799  tanatan  26883  atanbndlem  26889  amgmlem  26953  basellem3  27046  basellem5  27048  mpodvdsmulf1o  27157  dvdsmulf1o  27159  chtub  27175  fsumvma  27176  lgsquad2lem1  27347  2sqlem8  27389  dchrmusum2  27457  logsqvma  27505  pntrlog2bndlem4  27543  pw2divsnegd  28441  miriso  28738  lmieu  28852  ttgcontlem1  28953  brbtwn2  28974  ax5seglem1  28997  axcontlem2  29034  axcontlem4  29036  clwwlkel  30116  vc0  30645  hvsubdistr2  31121  adjlnop  32157  adjcoi  32171  cnvbraval  32181  fpwrelmap  32806  fsumiunle  32902  xrge0adddir  33078  cycpm2tr  33180  cycpmco2lem4  33190  cycpmco2lem7  33193  cyc3genpmlem  33212  archirngz  33250  archiabllem1b  33253  erler  33326  qusrn  33469  ressply10g  33627  ply1gsumz  33659  vietalem  33723  fedgmullem1  33773  fedgmullem2  33774  dimlssid  33776  constrrtcc  33879  rspectopn  34011  xrge0pluscn  34084  esumfzf  34213  esumiun  34238  volmeas  34375  omssubadd  34444  breprexplemc  34776  bnj553  35040  cvmliftlem6  35472  cvmliftlem10  35476  cvmlift2lem3  35487  finxpreclem4  37710  sin2h  37931  matunitlindflem2  37938  poimirlem16  37957  heibor  38142  ghomdiv  38213  3atlem1  39929  atmod3i2  40311  trljat2  40613  cdleme1  40673  cdleme22eALTN  40791  cdlemh2  41262  dihglblem3N  41741  dih1dimatlem0  41774  djhlsmcl  41860  mapdpglem30  42148  hdmapneg  42292  hgmapval1  42339  hgmapmul  42341  sn-1ne2  42703  sn-addrid  42853  fltnltalem  43095  3cubeslem3r  43119  3cubeslem4  43121  proot1ex  43624  tfsconcatfv  43769  dirkerper  46524  fourierdlem83  46617  fourierdlem92  46626  sigarperm  47288  sigaradd  47294  cos5t  47327  fmtnorec1  48000  lincresunit3lem2  48956  itsclc0yqsollem1  49238  itsclinecirc0b  49250  fuco11bALT  49813  prstchomval  50034  sinhpcosh  50215  amgmwlem  50277