Theorem 3eqtr2rd 2806

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

Syntax hints:   → wi 4   = wceq 1652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743

This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758

This theorem is referenced by:  nneob  7937  xp1d2m1eqxm1d2  11532  negmod  12923  modeqmodmin  12948  faclbnd2  13282  cats1un  13719  cjmulval  14170  fsumsplit  14756  fzosump1  14766  bcxmas  14851  trireciplem  14878  geo2sum  14888  geo2lim  14890  geoisum1c  14895  mertenslem1  14899  fprodsplit  14979  risefallfac  15037  bpolydiflem  15067  eftlub  15121  tanadd  15179  addsin  15182  subsin  15183  subcos  15187  sadadd2lem2  15453  qredeu  15652  zsqrtelqelz  15745  4sqlem15  15942  rcaninv  16719  resssetc  17007  resscatc  17020  estrreslem1  17042  curfcl  17138  mulgaddcomlem  17829  conjghm  17955  gasubg  17998  dfod2  18245  efginvrel2  18404  efgcpbllemb  18434  odadd2  18518  frgpnabllem1  18542  srgbinomlem3  18809  pws1  18883  prdslmodd  19241  psrlmod  19675  znunithash  20185  frlmipval  20394  frlmlbs  20412  restcld  21256  clmneg  23159  rrxds  23470  itg2monolem1  23808  itgconst  23876  dvexp  24007  dvfsumabs  24077  dvtaylp  24415  taylthlem2  24419  tangtx  24549  logsqrt  24741  lawcoslem1  24836  chordthmlem2  24851  chordthmlem4  24853  tanatan  24937  atanbndlem  24943  amgmlem  25007  basellem3  25100  basellem5  25102  dvdsmulf1o  25211  chtub  25228  fsumvma  25229  lgsquad2lem1  25400  2sqlem8  25442  dchrmusum2  25474  logsqvma  25522  pntrlog2bndlem4  25560  miriso  25856  lmieu  25967  sacgr  26013  ttgcontlem1  26056  brbtwn2  26076  ax5seglem1  26099  axcontlem2  26136  axcontlem4  26138  vc0  27885  hvsubdistr2  28363  adjlnop  29401  adjcoi  29415  cnvbraval  29425  fpwrelmap  29957  fsumiunle  30024  xrge0adddir  30139  archirngz  30190  archiabllem1b  30193  xrge0pluscn  30433  esumfzf  30578  esumiun  30603  volmeas  30741  omssubadd  30809  breprexplemc  31161  bnj553  31416  cvmliftlem6  31720  cvmliftlem10  31724  cvmlift2lem3  31735  finxpreclem4  33664  sin2h  33823  matunitlindflem2  33830  poimirlem16  33849  heibor  34042  ghomdiv  34113  3atlem1  35439  atmod3i2  35821  trljat2  36123  cdleme1  36183  cdleme22eALTN  36301  cdlemh2  36772  dihglblem3N  37251  dih1dimatlem0  37284  djhlsmcl  37370  mapdpglem30  37658  hdmapneg  37802  hgmapval1  37849  hgmapmul  37851  proot1ex  38456  dirkerper  40950  fourierdlem83  41043  fourierdlem92  41052  sigarperm  41689  sigaradd  41695  fmtnorec1  42125  lincresunit3lem2  42938  sinhpcosh  43153  amgmwlem  43220