Theorem 3eqtr2rd 2771

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

Syntax hints:   → wi 4   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  nneob  8597  xp1d2m1eqxm1d2  12412  negmod  13857  modeqmodmin  13882  faclbnd2  14232  cats1un  14662  cjmulval  15087  fsumsplit  15683  fzosump1  15694  bcxmas  15777  trireciplem  15804  geo2sum  15815  geo2lim  15817  geoisum1c  15822  mertenslem1  15826  fprodsplit  15908  risefallfac  15966  bpolydiflem  15996  eftlub  16053  tanadd  16111  addsin  16114  subsin  16115  subcos  16119  sadadd2lem2  16396  qredeu  16604  zsqrtelqelz  16704  4sqlem15  16906  rcaninv  17732  resssetc  18030  resscatc  18047  curfcl  18169  mulgaddcomlem  19005  conjghm  19157  gasubg  19210  dfod2  19470  efginvrel2  19633  efgcpbllemb  19661  odadd2  19755  frgpnabllem1  19779  srgbinomlem3  20113  pws1  20210  prdslmodd  20851  znunithash  21450  frlmipval  21664  frlmlbs  21682  psrlmod  21845  restcld  23035  clmneg  24957  rrxds  25269  itg2monolem1  25627  itgconst  25696  dvexp  25833  dvfsumabs  25905  dvtaylp  26254  taylthlem2  26258  taylthlem2OLD  26259  tangtx  26390  logsqrt  26589  zrtelqelz  26644  lawcoslem1  26701  chordthmlem2  26719  chordthmlem4  26721  tanatan  26805  atanbndlem  26811  amgmlem  26876  basellem3  26969  basellem5  26971  mpodvdsmulf1o  27080  dvdsmulf1o  27082  chtub  27099  fsumvma  27100  lgsquad2lem1  27271  2sqlem8  27313  dchrmusum2  27381  logsqvma  27429  pntrlog2bndlem4  27467  pw2divsnegd  28308  miriso  28573  lmieu  28687  ttgcontlem1  28788  brbtwn2  28808  ax5seglem1  28831  axcontlem2  28868  axcontlem4  28870  clwwlkel  29948  vc0  30476  hvsubdistr2  30952  adjlnop  31988  adjcoi  32002  cnvbraval  32012  fpwrelmap  32629  fsumiunle  32727  xrge0adddir  32932  cycpm2tr  33049  cycpmco2lem4  33059  cycpmco2lem7  33062  cyc3genpmlem  33081  archirngz  33116  archiabllem1b  33119  erler  33189  qusrn  33353  ressply10g  33509  ply1gsumz  33537  fedgmullem1  33598  fedgmullem2  33599  dimlssid  33601  constrrtcc  33698  rspectopn  33830  xrge0pluscn  33903  esumfzf  34032  esumiun  34057  volmeas  34194  omssubadd  34264  breprexplemc  34596  bnj553  34861  cvmliftlem6  35250  cvmliftlem10  35254  cvmlift2lem3  35265  finxpreclem4  37355  sin2h  37577  matunitlindflem2  37584  poimirlem16  37603  heibor  37788  ghomdiv  37859  3atlem1  39450  atmod3i2  39832  trljat2  40134  cdleme1  40194  cdleme22eALTN  40312  cdlemh2  40783  dihglblem3N  41262  dih1dimatlem0  41295  djhlsmcl  41381  mapdpglem30  41669  hdmapneg  41813  hgmapval1  41860  hgmapmul  41862  sn-1ne2  42226  sn-addrid  42382  fltnltalem  42623  3cubeslem3r  42648  3cubeslem4  42650  proot1ex  43158  tfsconcatfv  43303  dirkerper  46067  fourierdlem83  46160  fourierdlem92  46169  sigarperm  46831  sigaradd  46837  fmtnorec1  47511  lincresunit3lem2  48442  itsclc0yqsollem1  48724  itsclinecirc0b  48736  fuco11bALT  49300  prstchomval  49521  sinhpcosh  49702  amgmwlem  49764