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 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 2155  ax-ext 2732

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

This theorem is used by:  nneob  8645  xp1d2m1eqxm1d2  12523  negmod  13981  modeqmodmin  14006  faclbnd2  14356  cats1un  14791  cjmulval  15233  fsumsplit  15828  fzosump1  15839  bcxmas  15925  trireciplem  15952  geo2sum  15963  geo2lim  15965  geoisum1c  15970  mertenslem1  15974  fprodsplit  16054  risefallfac  16112  bpolydiflem  16141  eftlub  16198  tanadd  16256  addsin  16259  subsin  16260  subcos  16264  sadadd2lem2  16541  qredeu  16749  zsqrtelqelz  16850  4sqlem15  17052  rcaninv  17884  resssetc  18182  resscatc  18199  curfcl  18321  mulgaddcomlem  19221  conjghm  19377  gasubg  19430  dfod2  19692  efginvrel2  19855  efgcpbllemb  19883  odadd2  19977  frgpnabllem1  20001  srgbinomlem3  20368  pws1  20466  prdslmodd  21154  znunithash  21778  frlmipval  21993  frlmlbs  22011  psrlmod  22175  matunitlindflem2  22903  restcld  23398  clmneg  25310  rrxds  25622  itg2monolem1  25979  itgconst  26047  dvexp  26181  dvfsumabs  26251  dvtaylp  26607  taylthlem2  26611  tangtx  26744  logsqrt  26942  zrtelqelz  26996  lawcoslem1  27053  chordthmlem2  27071  chordthmlem4  27073  tanatan  27157  atanbndlem  27163  amgmlem  27227  basellem3  27320  basellem5  27322  mpodvdsmulf1o  27431  dvdsmulf1o  27433  chtub  27449  fsumvma  27450  lgsquad2lem1  27621  2sqlem8  27663  dchrmusum2  27731  logsqvma  27779  pntrlog2bndlem4  27817  pw2divsnegd  28715  miriso  29022  lnssplnglem  29149  lmieu  29169  ttgcontlem1  29342  brbtwn2  29363  ax5seglem1  29386  axcontlem2  29423  axcontlem4  29425  clwwlkel  30517  vc0  31056  hvsubdistr2  31532  adjlnop  32568  adjcoi  32582  cnvbraval  32592  fpwrelmap  33205  fsumiunle  33300  xrge0adddir  33459  cycpm2tr  33560  cycpmco2lem4  33570  cycpmco2lem7  33573  cyc3genpmlem  33592  archirngz  33630  archiabllem1b  33633  erler  33706  qusrn  33839  ressply10g  33978  ply1gsumz  34010  selvply1rhm0  34037  vietalem  34090  fedgmullem1  34140  fedgmullem2  34141  dimlssid  34143  constrrtcc  34246  rspectopn  34378  xrge0pluscn  34451  esumfzf  34580  esumiun  34605  volmeas  34743  omssubadd  34812  breprexplemc  35141  bnj553  35408  cvmliftlem6  35870  cvmliftlem10  35874  cvmlift2lem3  35885  finxpreclem4  38149  sin2h  38365  poimirlem16  38386  heibor  38572  ghomdiv  38643  3atlem1  40357  atmod3i2  40739  trljat2  41041  cdleme1  41101  cdleme22eALTN  41219  cdlemh2  41690  dihglblem3N  42169  dih1dimatlem0  42202  djhlsmcl  42288  mapdpglem30  42576  hdmapneg  42720  hgmapval1  42767  hgmapmul  42769  sn-1ne2  43147  sn-addrid  43297  fltnltalem  43509  3cubeslem3r  43533  3cubeslem4  43535  proot1ex  44038  tfsconcatfv  44183  dirkerper  46925  fourierdlem49  46984  fourierdlem83  47018  fourierdlem92  47027  sigarperm  47689  sigaradd  47695  cos5t  47744  fmtnorec1  48441  lincresunit3lem2  49411  itsclc0yqsollem1  49693  itsclinecirc0b  49705  fuco11bALT  50265  prstchomval  50486  sinhpcosh  50667  amgmwlem  50821