Theorem 3eqtr2rd 2778

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

Syntax hints:   → wi 4   = wceq 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2728

This theorem is referenced by:  nneob  8584  xp1d2m1eqxm1d2  12395  negmod  13839  modeqmodmin  13864  faclbnd2  14214  cats1un  14644  cjmulval  15068  fsumsplit  15664  fzosump1  15675  bcxmas  15758  trireciplem  15785  geo2sum  15796  geo2lim  15798  geoisum1c  15803  mertenslem1  15807  fprodsplit  15889  risefallfac  15947  bpolydiflem  15977  eftlub  16034  tanadd  16092  addsin  16095  subsin  16096  subcos  16100  sadadd2lem2  16377  qredeu  16585  zsqrtelqelz  16685  4sqlem15  16887  rcaninv  17718  resssetc  18016  resscatc  18033  curfcl  18155  mulgaddcomlem  19027  conjghm  19178  gasubg  19231  dfod2  19493  efginvrel2  19656  efgcpbllemb  19684  odadd2  19778  frgpnabllem1  19802  srgbinomlem3  20163  pws1  20260  prdslmodd  20920  znunithash  21519  frlmipval  21734  frlmlbs  21752  psrlmod  21915  restcld  23116  clmneg  25037  rrxds  25349  itg2monolem1  25707  itgconst  25776  dvexp  25913  dvfsumabs  25985  dvtaylp  26334  taylthlem2  26338  taylthlem2OLD  26339  tangtx  26470  logsqrt  26669  zrtelqelz  26724  lawcoslem1  26781  chordthmlem2  26799  chordthmlem4  26801  tanatan  26885  atanbndlem  26891  amgmlem  26956  basellem3  27049  basellem5  27051  mpodvdsmulf1o  27160  dvdsmulf1o  27162  chtub  27179  fsumvma  27180  lgsquad2lem1  27351  2sqlem8  27393  dchrmusum2  27461  logsqvma  27509  pntrlog2bndlem4  27547  pw2divsnegd  28445  miriso  28742  lmieu  28856  ttgcontlem1  28957  brbtwn2  28978  ax5seglem1  29001  axcontlem2  29038  axcontlem4  29040  clwwlkel  30121  vc0  30649  hvsubdistr2  31125  adjlnop  32161  adjcoi  32175  cnvbraval  32185  fpwrelmap  32812  fsumiunle  32910  xrge0adddir  33100  cycpm2tr  33201  cycpmco2lem4  33211  cycpmco2lem7  33214  cyc3genpmlem  33233  archirngz  33271  archiabllem1b  33274  erler  33347  qusrn  33490  ressply10g  33648  ply1gsumz  33680  vietalem  33735  fedgmullem1  33786  fedgmullem2  33787  dimlssid  33789  constrrtcc  33892  rspectopn  34024  xrge0pluscn  34097  esumfzf  34226  esumiun  34251  volmeas  34388  omssubadd  34457  breprexplemc  34789  bnj553  35054  cvmliftlem6  35484  cvmliftlem10  35488  cvmlift2lem3  35499  finxpreclem4  37599  sin2h  37811  matunitlindflem2  37818  poimirlem16  37837  heibor  38022  ghomdiv  38093  3atlem1  39753  atmod3i2  40135  trljat2  40437  cdleme1  40497  cdleme22eALTN  40615  cdlemh2  41086  dihglblem3N  41565  dih1dimatlem0  41598  djhlsmcl  41684  mapdpglem30  41972  hdmapneg  42116  hgmapval1  42163  hgmapmul  42165  sn-1ne2  42530  sn-addrid  42686  fltnltalem  42915  3cubeslem3r  42939  3cubeslem4  42941  proot1ex  43448  tfsconcatfv  43593  dirkerper  46350  fourierdlem83  46443  fourierdlem92  46452  sigarperm  47114  sigaradd  47120  fmtnorec1  47793  lincresunit3lem2  48736  itsclc0yqsollem1  49018  itsclinecirc0b  49030  fuco11bALT  49593  prstchomval  49814  sinhpcosh  49995  amgmwlem  50057