Theorem 3eqtr2rd 2780

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

Syntax hints:   → wi 4   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-cleq 2725

This theorem is referenced by:  nneob  8655  xp1d2m1eqxm1d2  12466  negmod  13881  modeqmodmin  13906  faclbnd2  14251  cats1un  14671  cjmulval  15092  fsumsplit  15687  fzosump1  15698  bcxmas  15781  trireciplem  15808  geo2sum  15819  geo2lim  15821  geoisum1c  15826  mertenslem1  15830  fprodsplit  15910  risefallfac  15968  bpolydiflem  15998  eftlub  16052  tanadd  16110  addsin  16113  subsin  16114  subcos  16118  sadadd2lem2  16391  qredeu  16595  zsqrtelqelz  16694  4sqlem15  16892  rcaninv  17741  resssetc  18042  resscatc  18059  estrreslem1OLD  18089  curfcl  18185  mulgaddcomlem  18977  conjghm  19123  gasubg  19166  dfod2  19432  efginvrel2  19595  efgcpbllemb  19623  odadd2  19717  frgpnabllem1  19741  srgbinomlem3  20051  pws1  20138  prdslmodd  20580  znunithash  21120  frlmipval  21334  frlmlbs  21352  psrlmod  21521  restcld  22676  clmneg  24597  rrxds  24910  itg2monolem1  25268  itgconst  25336  dvexp  25470  dvfsumabs  25540  dvtaylp  25882  taylthlem2  25886  tangtx  26015  logsqrt  26212  lawcoslem1  26320  chordthmlem2  26338  chordthmlem4  26340  tanatan  26424  atanbndlem  26430  amgmlem  26494  basellem3  26587  basellem5  26589  dvdsmulf1o  26698  chtub  26715  fsumvma  26716  lgsquad2lem1  26887  2sqlem8  26929  dchrmusum2  26997  logsqvma  27045  pntrlog2bndlem4  27083  miriso  27921  lmieu  28035  ttgcontlem1  28142  brbtwn2  28163  ax5seglem1  28186  axcontlem2  28223  axcontlem4  28225  clwwlkel  29299  vc0  29827  hvsubdistr2  30303  adjlnop  31339  adjcoi  31353  cnvbraval  31363  fpwrelmap  31958  fsumiunle  32035  xrge0adddir  32193  cycpm2tr  32278  cycpmco2lem4  32288  cycpmco2lem7  32291  cyc3genpmlem  32310  archirngz  32335  archiabllem1b  32338  qusrn  32520  ressply10g  32656  ply1gsumz  32669  fedgmullem1  32714  fedgmullem2  32715  rspectopn  32847  xrge0pluscn  32920  esumfzf  33067  esumiun  33092  volmeas  33229  omssubadd  33299  breprexplemc  33644  bnj553  33909  cvmliftlem6  34281  cvmliftlem10  34285  cvmlift2lem3  34296  finxpreclem4  36275  sin2h  36478  matunitlindflem2  36485  poimirlem16  36504  heibor  36689  ghomdiv  36760  3atlem1  38354  atmod3i2  38736  trljat2  39038  cdleme1  39098  cdleme22eALTN  39216  cdlemh2  39687  dihglblem3N  40166  dih1dimatlem0  40199  djhlsmcl  40285  mapdpglem30  40573  hdmapneg  40717  hgmapval1  40764  hgmapmul  40766  sn-1ne2  41179  zrtelqelz  41235  sn-addrid  41293  fltnltalem  41404  3cubeslem3r  41425  3cubeslem4  41427  proot1ex  41943  tfsconcatfv  42091  dirkerper  44812  fourierdlem83  44905  fourierdlem92  44914  sigarperm  45576  sigaradd  45582  fmtnorec1  46205  lincresunit3lem2  47161  itsclc0yqsollem1  47448  itsclinecirc0b  47460  prstchomval  47694  sinhpcosh  47785  amgmwlem  47849