Theorem 3eqtr2rd 2779

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 2775	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2773	1 ⊢ (𝜑 → 𝐷 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541

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 1913  ax-6 1971  ax-7 2011  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-cleq 2724

This theorem is referenced by:  nneob  8657  xp1d2m1eqxm1d2  12468  negmod  13883  modeqmodmin  13908  faclbnd2  14253  cats1un  14673  cjmulval  15094  fsumsplit  15689  fzosump1  15700  bcxmas  15783  trireciplem  15810  geo2sum  15821  geo2lim  15823  geoisum1c  15828  mertenslem1  15832  fprodsplit  15912  risefallfac  15970  bpolydiflem  16000  eftlub  16054  tanadd  16112  addsin  16115  subsin  16116  subcos  16120  sadadd2lem2  16393  qredeu  16597  zsqrtelqelz  16696  4sqlem15  16894  rcaninv  17743  resssetc  18044  resscatc  18061  estrreslem1OLD  18091  curfcl  18187  mulgaddcomlem  18979  conjghm  19125  gasubg  19168  dfod2  19434  efginvrel2  19597  efgcpbllemb  19625  odadd2  19719  frgpnabllem1  19743  srgbinomlem3  20053  pws1  20142  prdslmodd  20585  znunithash  21126  frlmipval  21340  frlmlbs  21358  psrlmod  21527  restcld  22683  clmneg  24604  rrxds  24917  itg2monolem1  25275  itgconst  25343  dvexp  25477  dvfsumabs  25547  dvtaylp  25889  taylthlem2  25893  tangtx  26022  logsqrt  26219  lawcoslem1  26327  chordthmlem2  26345  chordthmlem4  26347  tanatan  26431  atanbndlem  26437  amgmlem  26501  basellem3  26594  basellem5  26596  dvdsmulf1o  26705  chtub  26722  fsumvma  26723  lgsquad2lem1  26894  2sqlem8  26936  dchrmusum2  27004  logsqvma  27052  pntrlog2bndlem4  27090  miriso  27959  lmieu  28073  ttgcontlem1  28180  brbtwn2  28201  ax5seglem1  28224  axcontlem2  28261  axcontlem4  28263  clwwlkel  29337  vc0  29865  hvsubdistr2  30341  adjlnop  31377  adjcoi  31391  cnvbraval  31401  fpwrelmap  31996  fsumiunle  32073  xrge0adddir  32231  cycpm2tr  32319  cycpmco2lem4  32329  cycpmco2lem7  32332  cyc3genpmlem  32351  archirngz  32376  archiabllem1b  32379  qusrn  32565  ressply10g  32701  ply1gsumz  32715  fedgmullem1  32773  fedgmullem2  32774  rspectopn  32916  xrge0pluscn  32989  esumfzf  33136  esumiun  33161  volmeas  33298  omssubadd  33368  breprexplemc  33713  bnj553  33978  cvmliftlem6  34350  cvmliftlem10  34354  cvmlift2lem3  34365  finxpreclem4  36361  sin2h  36564  matunitlindflem2  36571  poimirlem16  36590  heibor  36775  ghomdiv  36846  3atlem1  38440  atmod3i2  38822  trljat2  39124  cdleme1  39184  cdleme22eALTN  39302  cdlemh2  39773  dihglblem3N  40252  dih1dimatlem0  40285  djhlsmcl  40371  mapdpglem30  40659  hdmapneg  40803  hgmapval1  40850  hgmapmul  40852  sn-1ne2  41261  zrtelqelz  41317  sn-addrid  41375  fltnltalem  41486  3cubeslem3r  41507  3cubeslem4  41509  proot1ex  42025  tfsconcatfv  42173  dirkerper  44891  fourierdlem83  44984  fourierdlem92  44993  sigarperm  45655  sigaradd  45661  fmtnorec1  46284  lincresunit3lem2  47239  itsclc0yqsollem1  47526  itsclinecirc0b  47538  prstchomval  47772  sinhpcosh  47863  amgmwlem  47927