Theorem 3eqtr2rd 2802

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752

This theorem is used by:  nneob  8673  xp1d2m1eqxm1d2  12607  negmod  14066  modeqmodmin  14091  faclbnd2  14442  cats1un  14878  cjmulval  15321  fsumsplit  15916  fzosump1  15927  bcxmas  16013  trireciplem  16040  geo2sum  16051  geo2lim  16053  geoisum1c  16058  mertenslem1  16062  fprodsplit  16142  risefallfac  16200  bpolydiflem  16229  eftlub  16286  tanadd  16344  addsin  16347  subsin  16348  subcos  16352  sadadd2lem2  16629  qredeu  16842  zsqrtelqelz  16943  4sqlem15  17146  rcaninv  17978  resssetc  18276  resscatc  18293  curfcl  18415  mulgaddcomlem  19316  conjghm  19472  gasubg  19525  dfod2  19787  efginvrel2  19950  efgcpbllemb  19978  odadd2  20072  frgpnabllem1  20096  srgbinomlem3  20463  pws1  20563  prdslmodd  21253  znunithash  21879  frlmipval  22094  frlmlbs  22112  psrlmod  22276  matunitlindflem2  23004  restcld  23499  clmneg  25411  rrxds  25723  itg2monolem1  26080  itgconst  26148  dvexp  26282  dvfsumabs  26352  dvtaylp  26706  taylthlem2  26710  tangtx  26843  logsqrt  27041  zrtelqelz  27095  lawcoslem1  27152  chordthmlem2  27170  chordthmlem4  27172  tanatan  27256  atanbndlem  27262  amgmlem  27326  basellem3  27419  basellem5  27421  mpodvdsmulf1o  27530  dvdsmulf1o  27532  chtub  27548  fsumvma  27549  lgsquad2lem1  27720  2sqlem8  27762  dchrmusum2  27830  logsqvma  27878  pntrlog2bndlem4  27916  pw2divsnegd  28844  miriso  29151  lnssplnglem  29278  lmieu  29298  ttgcontlem1  29471  brbtwn2  29492  ax5seglem1  29515  axcontlem2  29552  axcontlem4  29554  clwwlkel  30646  vc0  31185  hvsubdistr2  31661  adjlnop  32697  adjcoi  32711  cnvbraval  32721  fpwrelmap  33375  fsumiunle  33470  xrge0adddir  33629  cycpm2tr  33730  cycpmco2lem4  33740  cycpmco2lem7  33743  cyc3genpmlem  33762  archirngz  33800  archiabllem1b  33803  erler  33876  qusrn  34010  ressply10g  34149  ply1gsumz  34181  selvply1rhm0  34208  vietalem  34261  fedgmullem1  34311  fedgmullem2  34312  dimlssid  34314  constrrtcc  34417  rspectopn  34549  xrge0pluscn  34622  esumfzf  34751  esumiun  34776  volmeas  34914  omssubadd  34982  breprexplemc  35311  bnj553  35578  cvmliftlem6  36173  cvmliftlem10  36177  cvmlift2lem3  36188  finxpreclem4  38454  sin2h  38670  poimirlem16  38691  heibor  38892  ghomdiv  38963  3atlem1  40677  atmod3i2  41059  trljat2  41361  cdleme1  41421  cdleme22eALTN  41539  cdlemh2  42010  dihglblem3N  42489  dih1dimatlem0  42522  djhlsmcl  42608  mapdpglem30  42896  hdmapneg  43040  hgmapval1  43087  hgmapmul  43089  sn-1ne2  43467  sn-addrid  43609  fltnltalem  43810  3cubeslem3r  43834  3cubeslem4  43836  proot1ex  44335  tfsconcatfv  44480  dirkerper  47242  fourierdlem49  47301  fourierdlem83  47335  fourierdlem92  47344  sigarperm  48006  sigaradd  48012  cos5t  48061  fmtnorec1  48758  lincresunit3lem2  49728  itsclc0yqsollem1  50010  itsclinecirc0b  50022  fuco11bALT  50596  prstchomval  50833  sinhpcosh  51044  amgmwlem  51198