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 1540

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 1912  ax-6 1970  ax-7 2010  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723

This theorem is referenced by:  nneob  8658  xp1d2m1eqxm1d2  12471  negmod  13886  modeqmodmin  13911  faclbnd2  14256  cats1un  14676  cjmulval  15097  fsumsplit  15692  fzosump1  15703  bcxmas  15786  trireciplem  15813  geo2sum  15824  geo2lim  15826  geoisum1c  15831  mertenslem1  15835  fprodsplit  15915  risefallfac  15973  bpolydiflem  16003  eftlub  16057  tanadd  16115  addsin  16118  subsin  16119  subcos  16123  sadadd2lem2  16396  qredeu  16600  zsqrtelqelz  16699  4sqlem15  16897  rcaninv  17746  resssetc  18047  resscatc  18064  estrreslem1OLD  18094  curfcl  18190  mulgaddcomlem  19014  conjghm  19164  gasubg  19208  dfod2  19474  efginvrel2  19637  efgcpbllemb  19665  odadd2  19759  frgpnabllem1  19783  srgbinomlem3  20123  pws1  20214  prdslmodd  20725  znunithash  21340  frlmipval  21554  frlmlbs  21572  psrlmod  21741  restcld  22897  clmneg  24829  rrxds  25142  itg2monolem1  25501  itgconst  25569  dvexp  25703  dvfsumabs  25773  dvtaylp  26115  taylthlem2  26119  tangtx  26248  logsqrt  26445  lawcoslem1  26553  chordthmlem2  26571  chordthmlem4  26573  tanatan  26657  atanbndlem  26663  amgmlem  26727  basellem3  26820  basellem5  26822  dvdsmulf1o  26931  chtub  26948  fsumvma  26949  lgsquad2lem1  27120  2sqlem8  27162  dchrmusum2  27230  logsqvma  27278  pntrlog2bndlem4  27316  miriso  28185  lmieu  28299  ttgcontlem1  28406  brbtwn2  28427  ax5seglem1  28450  axcontlem2  28487  axcontlem4  28489  clwwlkel  29563  vc0  30091  hvsubdistr2  30567  adjlnop  31603  adjcoi  31617  cnvbraval  31627  fpwrelmap  32222  fsumiunle  32299  xrge0adddir  32457  cycpm2tr  32545  cycpmco2lem4  32555  cycpmco2lem7  32558  cyc3genpmlem  32577  archirngz  32602  archiabllem1b  32605  qusrn  32791  ressply10g  32927  ply1gsumz  32941  fedgmullem1  32999  fedgmullem2  33000  rspectopn  33142  xrge0pluscn  33215  esumfzf  33362  esumiun  33387  volmeas  33524  omssubadd  33594  breprexplemc  33939  bnj553  34204  cvmliftlem6  34576  cvmliftlem10  34580  cvmlift2lem3  34591  finxpreclem4  36579  sin2h  36782  matunitlindflem2  36789  poimirlem16  36808  heibor  36993  ghomdiv  37064  3atlem1  38658  atmod3i2  39040  trljat2  39342  cdleme1  39402  cdleme22eALTN  39520  cdlemh2  39991  dihglblem3N  40470  dih1dimatlem0  40503  djhlsmcl  40589  mapdpglem30  40877  hdmapneg  41021  hgmapval1  41068  hgmapmul  41070  sn-1ne2  41482  zrtelqelz  41538  sn-addrid  41596  fltnltalem  41707  3cubeslem3r  41728  3cubeslem4  41730  proot1ex  42246  tfsconcatfv  42394  dirkerper  45112  fourierdlem83  45205  fourierdlem92  45214  sigarperm  45876  sigaradd  45882  fmtnorec1  46505  lincresunit3lem2  47250  itsclc0yqsollem1  47537  itsclinecirc0b  47549  prstchomval  47783  sinhpcosh  47874  amgmwlem  47938