Theorem 3eqtr2rd 2808

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2758

This theorem is used by:  nneob  8651  xp1d2m1eqxm1d2  12516  negmod  13972  modeqmodmin  13997  faclbnd2  14347  cats1un  14782  cjmulval  15222  fsumsplit  15818  fzosump1  15829  bcxmas  15915  trireciplem  15942  geo2sum  15953  geo2lim  15955  geoisum1c  15960  mertenslem1  15964  fprodsplit  16046  risefallfac  16104  bpolydiflem  16133  eftlub  16190  tanadd  16248  addsin  16251  subsin  16252  subcos  16256  sadadd2lem2  16533  qredeu  16741  zsqrtelqelz  16842  4sqlem15  17044  rcaninv  17876  resssetc  18174  resscatc  18191  curfcl  18313  mulgaddcomlem  19188  conjghm  19344  gasubg  19397  dfod2  19659  efginvrel2  19822  efgcpbllemb  19850  odadd2  19944  frgpnabllem1  19968  srgbinomlem3  20335  pws1  20432  prdslmodd  21120  znunithash  21744  frlmipval  21959  frlmlbs  21977  psrlmod  22139  restcld  23359  clmneg  25270  rrxds  25582  itg2monolem1  25939  itgconst  26008  dvexp  26142  dvfsumabs  26212  dvtaylp  26563  taylthlem2  26567  tangtx  26700  logsqrt  26899  zrtelqelz  26953  lawcoslem1  27010  chordthmlem2  27028  chordthmlem4  27030  tanatan  27114  atanbndlem  27120  amgmlem  27184  basellem3  27277  basellem5  27279  mpodvdsmulf1o  27388  dvdsmulf1o  27390  chtub  27406  fsumvma  27407  lgsquad2lem1  27578  2sqlem8  27620  dchrmusum2  27688  logsqvma  27736  pntrlog2bndlem4  27774  pw2divsnegd  28672  miriso  28977  lnssplnglem  29103  lmieu  29123  ttgcontlem1  29264  brbtwn2  29285  ax5seglem1  29308  axcontlem2  29345  axcontlem4  29347  clwwlkel  30427  vc0  30956  hvsubdistr2  31432  adjlnop  32468  adjcoi  32482  cnvbraval  32492  fpwrelmap  33108  fsumiunle  33203  xrge0adddir  33362  cycpm2tr  33463  cycpmco2lem4  33473  cycpmco2lem7  33476  cyc3genpmlem  33495  archirngz  33533  archiabllem1b  33536  erler  33609  qusrn  33742  ressply10g  33881  ply1gsumz  33913  selvply1rhm0  33940  vietalem  33993  fedgmullem1  34043  fedgmullem2  34044  dimlssid  34046  constrrtcc  34149  rspectopn  34281  xrge0pluscn  34354  esumfzf  34483  esumiun  34508  volmeas  34645  omssubadd  34714  breprexplemc  35043  bnj553  35310  cvmliftlem6  35795  cvmliftlem10  35799  cvmlift2lem3  35810  finxpreclem4  38073  sin2h  38294  matunitlindflem2  38301  poimirlem16  38320  heibor  38505  ghomdiv  38576  3atlem1  40290  atmod3i2  40672  trljat2  40974  cdleme1  41034  cdleme22eALTN  41152  cdlemh2  41623  dihglblem3N  42102  dih1dimatlem0  42135  djhlsmcl  42221  mapdpglem30  42509  hdmapneg  42653  hgmapval1  42700  hgmapmul  42702  sn-1ne2  43065  sn-addrid  43215  fltnltalem  43427  3cubeslem3r  43451  3cubeslem4  43453  proot1ex  43956  tfsconcatfv  44101  dirkerper  46843  fourierdlem49  46902  fourierdlem83  46936  fourierdlem92  46945  sigarperm  47607  sigaradd  47613  cos5t  47649  fmtnorec1  48322  lincresunit3lem2  49293  itsclc0yqsollem1  49575  itsclinecirc0b  49587  fuco11bALT  50149  prstchomval  50370  sinhpcosh  50551  amgmwlem  50683