Theorem 3eqtr2rd 2773

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 2769	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2767	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 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  nneob  8571  xp1d2m1eqxm1d2  12375  negmod  13823  modeqmodmin  13848  faclbnd2  14198  cats1un  14628  cjmulval  15052  fsumsplit  15648  fzosump1  15659  bcxmas  15742  trireciplem  15769  geo2sum  15780  geo2lim  15782  geoisum1c  15787  mertenslem1  15791  fprodsplit  15873  risefallfac  15931  bpolydiflem  15961  eftlub  16018  tanadd  16076  addsin  16079  subsin  16080  subcos  16084  sadadd2lem2  16361  qredeu  16569  zsqrtelqelz  16669  4sqlem15  16871  rcaninv  17701  resssetc  17999  resscatc  18016  curfcl  18138  mulgaddcomlem  19010  conjghm  19161  gasubg  19214  dfod2  19476  efginvrel2  19639  efgcpbllemb  19667  odadd2  19761  frgpnabllem1  19785  srgbinomlem3  20146  pws1  20243  prdslmodd  20902  znunithash  21501  frlmipval  21716  frlmlbs  21734  psrlmod  21897  restcld  23087  clmneg  25008  rrxds  25320  itg2monolem1  25678  itgconst  25747  dvexp  25884  dvfsumabs  25956  dvtaylp  26305  taylthlem2  26309  taylthlem2OLD  26310  tangtx  26441  logsqrt  26640  zrtelqelz  26695  lawcoslem1  26752  chordthmlem2  26770  chordthmlem4  26772  tanatan  26856  atanbndlem  26862  amgmlem  26927  basellem3  27020  basellem5  27022  mpodvdsmulf1o  27131  dvdsmulf1o  27133  chtub  27150  fsumvma  27151  lgsquad2lem1  27322  2sqlem8  27364  dchrmusum2  27432  logsqvma  27480  pntrlog2bndlem4  27518  pw2divsnegd  28372  miriso  28648  lmieu  28762  ttgcontlem1  28863  brbtwn2  28883  ax5seglem1  28906  axcontlem2  28943  axcontlem4  28945  clwwlkel  30026  vc0  30554  hvsubdistr2  31030  adjlnop  32066  adjcoi  32080  cnvbraval  32090  fpwrelmap  32716  fsumiunle  32812  xrge0adddir  32999  cycpm2tr  33088  cycpmco2lem4  33098  cycpmco2lem7  33101  cyc3genpmlem  33120  archirngz  33158  archiabllem1b  33161  erler  33232  qusrn  33374  ressply10g  33530  ply1gsumz  33559  fedgmullem1  33642  fedgmullem2  33643  dimlssid  33645  constrrtcc  33748  rspectopn  33880  xrge0pluscn  33953  esumfzf  34082  esumiun  34107  volmeas  34244  omssubadd  34313  breprexplemc  34645  bnj553  34910  cvmliftlem6  35334  cvmliftlem10  35338  cvmlift2lem3  35349  finxpreclem4  37438  sin2h  37660  matunitlindflem2  37667  poimirlem16  37686  heibor  37871  ghomdiv  37942  3atlem1  39592  atmod3i2  39974  trljat2  40276  cdleme1  40336  cdleme22eALTN  40454  cdlemh2  40925  dihglblem3N  41404  dih1dimatlem0  41437  djhlsmcl  41523  mapdpglem30  41811  hdmapneg  41955  hgmapval1  42002  hgmapmul  42004  sn-1ne2  42368  sn-addrid  42524  fltnltalem  42765  3cubeslem3r  42790  3cubeslem4  42792  proot1ex  43299  tfsconcatfv  43444  dirkerper  46204  fourierdlem83  46297  fourierdlem92  46306  sigarperm  46968  sigaradd  46974  fmtnorec1  47647  lincresunit3lem2  48591  itsclc0yqsollem1  48873  itsclinecirc0b  48885  fuco11bALT  49449  prstchomval  49670  sinhpcosh  49851  amgmwlem  49913