Theorem 3eqtr2rd 2772

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 2768	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2766	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 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717

This theorem is referenced by:  nneob  8677  xp1d2m1eqxm1d2  12504  negmod  13922  modeqmodmin  13947  faclbnd2  14291  cats1un  14712  cjmulval  15133  fsumsplit  15728  fzosump1  15739  bcxmas  15822  trireciplem  15849  geo2sum  15860  geo2lim  15862  geoisum1c  15867  mertenslem1  15871  fprodsplit  15951  risefallfac  16009  bpolydiflem  16039  eftlub  16094  tanadd  16152  addsin  16155  subsin  16156  subcos  16160  sadadd2lem2  16433  qredeu  16637  zsqrtelqelz  16738  4sqlem15  16936  rcaninv  17785  resssetc  18089  resscatc  18106  estrreslem1OLD  18136  curfcl  18232  mulgaddcomlem  19065  conjghm  19217  gasubg  19270  dfod2  19536  efginvrel2  19699  efgcpbllemb  19727  odadd2  19821  frgpnabllem1  19845  srgbinomlem3  20185  pws1  20278  prdslmodd  20870  znunithash  21520  frlmipval  21735  frlmlbs  21753  psrlmod  21927  restcld  23125  clmneg  25057  rrxds  25370  itg2monolem1  25729  itgconst  25797  dvexp  25934  dvfsumabs  26006  dvtaylp  26355  taylthlem2  26359  taylthlem2OLD  26360  tangtx  26490  logsqrt  26688  lawcoslem1  26797  chordthmlem2  26815  chordthmlem4  26817  tanatan  26901  atanbndlem  26907  amgmlem  26972  basellem3  27065  basellem5  27067  mpodvdsmulf1o  27176  dvdsmulf1o  27178  chtub  27195  fsumvma  27196  lgsquad2lem1  27367  2sqlem8  27409  dchrmusum2  27477  logsqvma  27525  pntrlog2bndlem4  27563  miriso  28551  lmieu  28665  ttgcontlem1  28772  brbtwn2  28793  ax5seglem1  28816  axcontlem2  28853  axcontlem4  28855  clwwlkel  29933  vc0  30461  hvsubdistr2  30937  adjlnop  31973  adjcoi  31987  cnvbraval  31997  fpwrelmap  32602  fsumiunle  32682  xrge0adddir  32842  cycpm2tr  32937  cycpmco2lem4  32947  cycpmco2lem7  32950  cyc3genpmlem  32969  archirngz  32994  archiabllem1b  32997  erler  33060  qusrn  33226  ressply10g  33381  ply1gsumz  33402  fedgmullem1  33460  fedgmullem2  33461  rspectopn  33601  xrge0pluscn  33674  esumfzf  33821  esumiun  33846  volmeas  33983  omssubadd  34053  breprexplemc  34397  bnj553  34662  cvmliftlem6  35033  cvmliftlem10  35037  cvmlift2lem3  35048  finxpreclem4  37006  sin2h  37216  matunitlindflem2  37223  poimirlem16  37242  heibor  37427  ghomdiv  37498  3atlem1  39088  atmod3i2  39470  trljat2  39772  cdleme1  39832  cdleme22eALTN  39950  cdlemh2  40421  dihglblem3N  40900  dih1dimatlem0  40933  djhlsmcl  41019  mapdpglem30  41307  hdmapneg  41451  hgmapval1  41498  hgmapmul  41500  sn-1ne2  41977  zrtelqelz  42041  sn-addrid  42112  fltnltalem  42223  3cubeslem3r  42251  3cubeslem4  42253  proot1ex  42768  tfsconcatfv  42914  dirkerper  45624  fourierdlem83  45717  fourierdlem92  45726  sigarperm  46388  sigaradd  46394  fmtnorec1  47016  lincresunit3lem2  47736  itsclc0yqsollem1  48023  itsclinecirc0b  48035  prstchomval  48268  sinhpcosh  48359  amgmwlem  48423