Theorem 3eqtr2rd 2811

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

Syntax hints:   → wi 4   = wceq 1567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761

This theorem is referenced by:  nneob  8642  xp1d2m1eqxm1d2  12498  negmod  13952  modeqmodmin  13977  faclbnd2  14327  cats1un  14758  cjmulval  15196  fsumsplit  15792  fzosump1  15803  bcxmas  15889  trireciplem  15916  geo2sum  15927  geo2lim  15929  geoisum1c  15934  mertenslem1  15938  fprodsplit  16020  risefallfac  16078  bpolydiflem  16108  eftlub  16165  tanadd  16223  addsin  16226  subsin  16227  subcos  16231  sadadd2lem2  16508  qredeu  16716  zsqrtelqelz  16817  4sqlem15  17019  rcaninv  17851  resssetc  18149  resscatc  18166  curfcl  18288  mulgaddcomlem  19163  conjghm  19319  gasubg  19372  dfod2  19634  efginvrel2  19797  efgcpbllemb  19825  odadd2  19919  frgpnabllem1  19943  srgbinomlem3  20310  pws1  20406  prdslmodd  21068  znunithash  21683  frlmipval  21898  frlmlbs  21916  psrlmod  22078  restcld  23298  clmneg  25209  rrxds  25521  itg2monolem1  25878  itgconst  25947  dvexp  26081  dvfsumabs  26151  dvtaylp  26499  taylthlem2  26503  tangtx  26636  logsqrt  26835  zrtelqelz  26889  lawcoslem1  26946  chordthmlem2  26964  chordthmlem4  26966  tanatan  27050  atanbndlem  27056  amgmlem  27120  basellem3  27213  basellem5  27215  mpodvdsmulf1o  27324  dvdsmulf1o  27326  chtub  27342  fsumvma  27343  lgsquad2lem1  27514  2sqlem8  27556  dchrmusum2  27624  logsqvma  27672  pntrlog2bndlem4  27710  pw2divsnegd  28608  miriso  28909  lnssplnglem  29031  lmieu  29051  ttgcontlem1  29175  brbtwn2  29196  ax5seglem1  29219  axcontlem2  29256  axcontlem4  29258  clwwlkel  30338  vc0  30867  hvsubdistr2  31343  adjlnop  32379  adjcoi  32393  cnvbraval  32403  fpwrelmap  33019  fsumiunle  33114  xrge0adddir  33279  cycpm2tr  33380  cycpmco2lem4  33390  cycpmco2lem7  33393  cyc3genpmlem  33412  archirngz  33450  archiabllem1b  33453  erler  33526  qusrn  33662  ressply10g  33802  ply1gsumz  33834  selvply1rhm0  33861  vietalem  33914  fedgmullem1  33964  fedgmullem2  33965  dimlssid  33967  constrrtcc  34070  rspectopn  34202  xrge0pluscn  34275  esumfzf  34404  esumiun  34429  volmeas  34566  omssubadd  34635  breprexplemc  34964  bnj553  35231  cvmliftlem6  35681  cvmliftlem10  35685  cvmlift2lem3  35696  finxpreclem4  37928  sin2h  38149  matunitlindflem2  38156  poimirlem16  38175  heibor  38360  ghomdiv  38431  3atlem1  40147  atmod3i2  40529  trljat2  40831  cdleme1  40891  cdleme22eALTN  41009  cdlemh2  41480  dihglblem3N  41959  dih1dimatlem0  41992  djhlsmcl  42078  mapdpglem30  42366  hdmapneg  42510  hgmapval1  42557  hgmapmul  42559  sn-1ne2  42922  sn-addrid  43072  fltnltalem  43286  3cubeslem3r  43310  3cubeslem4  43312  proot1ex  43815  tfsconcatfv  43960  dirkerper  46702  fourierdlem49  46761  fourierdlem83  46795  fourierdlem92  46804  sigarperm  47466  sigaradd  47472  cos5t  47505  fmtnorec1  48178  lincresunit3lem2  49145  itsclc0yqsollem1  49427  itsclinecirc0b  49439  fuco11bALT  50001  prstchomval  50222  sinhpcosh  50403  amgmwlem  50476