Theorem 3eqtr2rd 2781

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

Syntax hints:   → wi 4   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  nneob  8582  xp1d2m1eqxm1d2  12422  negmod  13869  modeqmodmin  13894  faclbnd2  14244  cats1un  14674  cjmulval  15098  fsumsplit  15694  fzosump1  15705  bcxmas  15791  trireciplem  15818  geo2sum  15829  geo2lim  15831  geoisum1c  15836  mertenslem1  15840  fprodsplit  15922  risefallfac  15980  bpolydiflem  16010  eftlub  16067  tanadd  16125  addsin  16128  subsin  16129  subcos  16133  sadadd2lem2  16410  qredeu  16618  zsqrtelqelz  16719  4sqlem15  16921  rcaninv  17752  resssetc  18050  resscatc  18067  curfcl  18189  mulgaddcomlem  19064  conjghm  19215  gasubg  19268  dfod2  19530  efginvrel2  19693  efgcpbllemb  19721  odadd2  19815  frgpnabllem1  19839  srgbinomlem3  20200  pws1  20295  prdslmodd  20959  znunithash  21539  frlmipval  21754  frlmlbs  21772  psrlmod  21934  restcld  23155  clmneg  25066  rrxds  25378  itg2monolem1  25735  itgconst  25804  dvexp  25938  dvfsumabs  26008  dvtaylp  26353  taylthlem2  26357  tangtx  26487  logsqrt  26686  zrtelqelz  26740  lawcoslem1  26797  chordthmlem2  26815  chordthmlem4  26817  tanatan  26901  atanbndlem  26907  amgmlem  26971  basellem3  27064  basellem5  27066  mpodvdsmulf1o  27175  dvdsmulf1o  27177  chtub  27193  fsumvma  27194  lgsquad2lem1  27365  2sqlem8  27407  dchrmusum2  27475  logsqvma  27523  pntrlog2bndlem4  27561  pw2divsnegd  28459  miriso  28756  lmieu  28870  ttgcontlem1  28971  brbtwn2  28992  ax5seglem1  29015  axcontlem2  29052  axcontlem4  29054  clwwlkel  30134  vc0  30663  hvsubdistr2  31139  adjlnop  32175  adjcoi  32189  cnvbraval  32199  fpwrelmap  32825  fsumiunle  32921  xrge0adddir  33097  cycpm2tr  33200  cycpmco2lem4  33210  cycpmco2lem7  33213  cyc3genpmlem  33232  archirngz  33270  archiabllem1b  33273  erler  33346  qusrn  33492  ressply10g  33650  ply1gsumz  33682  selvply1rhm0  33710  vietalem  33763  fedgmullem1  33813  fedgmullem2  33814  dimlssid  33816  constrrtcc  33919  rspectopn  34051  xrge0pluscn  34124  esumfzf  34253  esumiun  34278  volmeas  34415  omssubadd  34484  breprexplemc  34816  bnj553  35080  cvmliftlem6  35518  cvmliftlem10  35522  cvmlift2lem3  35533  finxpreclem4  37756  sin2h  37977  matunitlindflem2  37984  poimirlem16  38003  heibor  38188  ghomdiv  38259  3atlem1  39975  atmod3i2  40357  trljat2  40659  cdleme1  40719  cdleme22eALTN  40837  cdlemh2  41308  dihglblem3N  41787  dih1dimatlem0  41820  djhlsmcl  41906  mapdpglem30  42194  hdmapneg  42338  hgmapval1  42385  hgmapmul  42387  sn-1ne2  42748  sn-addrid  42898  fltnltalem  43112  3cubeslem3r  43136  3cubeslem4  43138  proot1ex  43641  tfsconcatfv  43786  dirkerper  46539  fourierdlem83  46632  fourierdlem92  46641  sigarperm  47303  sigaradd  47309  cos5t  47342  fmtnorec1  48015  lincresunit3lem2  48971  itsclc0yqsollem1  49253  itsclinecirc0b  49265  fuco11bALT  49828  prstchomval  50049  sinhpcosh  50230  amgmwlem  50292