Theorem 3eqtr2rd 2863

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

Syntax hints:   → wi 4   = wceq 1533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-9 2120  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1777  df-cleq 2814

This theorem is referenced by:  nneob  8273  xp1d2m1eqxm1d2  11885  negmod  13278  modeqmodmin  13303  faclbnd2  13645  cats1un  14077  cjmulval  14498  fsumsplit  15091  fzosump1  15101  bcxmas  15184  trireciplem  15211  geo2sum  15223  geo2lim  15225  geoisum1c  15230  mertenslem1  15234  fprodsplit  15314  risefallfac  15372  bpolydiflem  15402  eftlub  15456  tanadd  15514  addsin  15517  subsin  15518  subcos  15522  sadadd2lem2  15793  qredeu  15996  zsqrtelqelz  16092  4sqlem15  16289  rcaninv  17058  resssetc  17346  resscatc  17359  estrreslem1  17381  curfcl  17476  mulgaddcomlem  18244  conjghm  18383  gasubg  18426  dfod2  18685  efginvrel2  18847  efgcpbllemb  18875  odadd2  18963  frgpnabllem1  18987  srgbinomlem3  19286  pws1  19360  prdslmodd  19735  psrlmod  20175  znunithash  20705  frlmipval  20917  frlmlbs  20935  restcld  21774  clmneg  23679  rrxds  23990  itg2monolem1  24345  itgconst  24413  dvexp  24544  dvfsumabs  24614  dvtaylp  24952  taylthlem2  24956  tangtx  25085  logsqrt  25281  lawcoslem1  25387  chordthmlem2  25405  chordthmlem4  25407  tanatan  25491  atanbndlem  25497  amgmlem  25561  basellem3  25654  basellem5  25656  dvdsmulf1o  25765  chtub  25782  fsumvma  25783  lgsquad2lem1  25954  2sqlem8  25996  dchrmusum2  26064  logsqvma  26112  pntrlog2bndlem4  26150  miriso  26450  lmieu  26564  ttgcontlem1  26665  brbtwn2  26685  ax5seglem1  26708  axcontlem2  26745  axcontlem4  26747  clwwlkel  27819  vc0  28345  hvsubdistr2  28821  adjlnop  29857  adjcoi  29871  cnvbraval  29881  fpwrelmap  30463  fsumiunle  30540  xrge0adddir  30674  cycpm2tr  30756  cycpmco2lem4  30766  cycpmco2lem7  30769  cyc3genpmlem  30788  archirngz  30813  archiabllem1b  30816  fedgmullem1  31020  fedgmullem2  31021  xrge0pluscn  31178  esumfzf  31323  esumiun  31348  volmeas  31485  omssubadd  31553  breprexplemc  31898  bnj553  32165  cvmliftlem6  32532  cvmliftlem10  32536  cvmlift2lem3  32547  finxpreclem4  34669  sin2h  34876  matunitlindflem2  34883  poimirlem16  34902  heibor  35093  ghomdiv  35164  3atlem1  36613  atmod3i2  36995  trljat2  37297  cdleme1  37357  cdleme22eALTN  37475  cdlemh2  37946  dihglblem3N  38425  dih1dimatlem0  38458  djhlsmcl  38544  mapdpglem30  38832  hdmapneg  38976  hgmapval1  39023  hgmapmul  39025  sn-1ne2  39151  zrtelqelz  39185  fltnltalem  39267  3cubeslem3r  39277  3cubeslem4  39279  proot1ex  39794  dirkerper  42375  fourierdlem83  42468  fourierdlem92  42477  sigarperm  43111  sigaradd  43117  fmtnorec1  43693  lincresunit3lem2  44529  itsclc0yqsollem1  44743  itsclinecirc0b  44755  sinhpcosh  44833  amgmwlem  44897