Theorem 3eqtr2rd 2840

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

Syntax hints:   → wi 4   = wceq 1538

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 1911  ax-6 1970  ax-7 2015  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791

This theorem is referenced by:  nneob  8262  xp1d2m1eqxm1d2  11879  negmod  13279  modeqmodmin  13304  faclbnd2  13647  cats1un  14074  cjmulval  14496  fsumsplit  15089  fzosump1  15099  bcxmas  15182  trireciplem  15209  geo2sum  15221  geo2lim  15223  geoisum1c  15228  mertenslem1  15232  fprodsplit  15312  risefallfac  15370  bpolydiflem  15400  eftlub  15454  tanadd  15512  addsin  15515  subsin  15516  subcos  15520  sadadd2lem2  15789  qredeu  15992  zsqrtelqelz  16088  4sqlem15  16285  rcaninv  17056  resssetc  17344  resscatc  17357  estrreslem1  17379  curfcl  17474  mulgaddcomlem  18242  conjghm  18381  gasubg  18424  dfod2  18683  efginvrel2  18845  efgcpbllemb  18873  odadd2  18962  frgpnabllem1  18986  srgbinomlem3  19285  pws1  19362  prdslmodd  19734  znunithash  20256  frlmipval  20468  frlmlbs  20486  psrlmod  20639  restcld  21777  clmneg  23686  rrxds  23997  itg2monolem1  24354  itgconst  24422  dvexp  24556  dvfsumabs  24626  dvtaylp  24965  taylthlem2  24969  tangtx  25098  logsqrt  25295  lawcoslem1  25401  chordthmlem2  25419  chordthmlem4  25421  tanatan  25505  atanbndlem  25511  amgmlem  25575  basellem3  25668  basellem5  25670  dvdsmulf1o  25779  chtub  25796  fsumvma  25797  lgsquad2lem1  25968  2sqlem8  26010  dchrmusum2  26078  logsqvma  26126  pntrlog2bndlem4  26164  miriso  26464  lmieu  26578  ttgcontlem1  26679  brbtwn2  26699  ax5seglem1  26722  axcontlem2  26759  axcontlem4  26761  clwwlkel  27831  vc0  28357  hvsubdistr2  28833  adjlnop  29869  adjcoi  29883  cnvbraval  29893  fpwrelmap  30495  fsumiunle  30571  xrge0adddir  30726  cycpm2tr  30811  cycpmco2lem4  30821  cycpmco2lem7  30824  cyc3genpmlem  30843  archirngz  30868  archiabllem1b  30871  fedgmullem1  31113  fedgmullem2  31114  rspectopn  31220  xrge0pluscn  31293  esumfzf  31438  esumiun  31463  volmeas  31600  omssubadd  31668  breprexplemc  32013  bnj553  32280  cvmliftlem6  32650  cvmliftlem10  32654  cvmlift2lem3  32665  finxpreclem4  34811  sin2h  35047  matunitlindflem2  35054  poimirlem16  35073  heibor  35259  ghomdiv  35330  3atlem1  36779  atmod3i2  37161  trljat2  37463  cdleme1  37523  cdleme22eALTN  37641  cdlemh2  38112  dihglblem3N  38591  dih1dimatlem0  38624  djhlsmcl  38710  mapdpglem30  38998  hdmapneg  39142  hgmapval1  39189  hgmapmul  39191  sn-1ne2  39466  zrtelqelz  39500  sn-addid1  39557  fltnltalem  39618  3cubeslem3r  39628  3cubeslem4  39630  proot1ex  40145  dirkerper  42738  fourierdlem83  42831  fourierdlem92  42840  sigarperm  43474  sigaradd  43480  fmtnorec1  44054  lincresunit3lem2  44889  itsclc0yqsollem1  45176  itsclinecirc0b  45188  sinhpcosh  45266  amgmwlem  45330