Theorem 3eqtr2rd 2779

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 2775	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4		3eqtr2d.3	. 2 ⊢ (𝜑 → 𝐶 = 𝐷)
5	3, 4	eqtr2d 2773	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 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  nneob  8594  xp1d2m1eqxm1d2  12407  negmod  13851  modeqmodmin  13876  faclbnd2  14226  cats1un  14656  cjmulval  15080  fsumsplit  15676  fzosump1  15687  bcxmas  15770  trireciplem  15797  geo2sum  15808  geo2lim  15810  geoisum1c  15815  mertenslem1  15819  fprodsplit  15901  risefallfac  15959  bpolydiflem  15989  eftlub  16046  tanadd  16104  addsin  16107  subsin  16108  subcos  16112  sadadd2lem2  16389  qredeu  16597  zsqrtelqelz  16697  4sqlem15  16899  rcaninv  17730  resssetc  18028  resscatc  18045  curfcl  18167  mulgaddcomlem  19039  conjghm  19190  gasubg  19243  dfod2  19505  efginvrel2  19668  efgcpbllemb  19696  odadd2  19790  frgpnabllem1  19814  srgbinomlem3  20175  pws1  20272  prdslmodd  20932  znunithash  21531  frlmipval  21746  frlmlbs  21764  psrlmod  21927  restcld  23128  clmneg  25049  rrxds  25361  itg2monolem1  25719  itgconst  25788  dvexp  25925  dvfsumabs  25997  dvtaylp  26346  taylthlem2  26350  taylthlem2OLD  26351  tangtx  26482  logsqrt  26681  zrtelqelz  26736  lawcoslem1  26793  chordthmlem2  26811  chordthmlem4  26813  tanatan  26897  atanbndlem  26903  amgmlem  26968  basellem3  27061  basellem5  27063  mpodvdsmulf1o  27172  dvdsmulf1o  27174  chtub  27191  fsumvma  27192  lgsquad2lem1  27363  2sqlem8  27405  dchrmusum2  27473  logsqvma  27521  pntrlog2bndlem4  27559  pw2divsnegd  28457  miriso  28754  lmieu  28868  ttgcontlem1  28969  brbtwn2  28990  ax5seglem1  29013  axcontlem2  29050  axcontlem4  29052  clwwlkel  30133  vc0  30662  hvsubdistr2  31138  adjlnop  32174  adjcoi  32188  cnvbraval  32198  fpwrelmap  32823  fsumiunle  32921  xrge0adddir  33111  cycpm2tr  33213  cycpmco2lem4  33223  cycpmco2lem7  33226  cyc3genpmlem  33245  archirngz  33283  archiabllem1b  33286  erler  33359  qusrn  33502  ressply10g  33660  ply1gsumz  33692  vietalem  33756  fedgmullem1  33807  fedgmullem2  33808  dimlssid  33810  constrrtcc  33913  rspectopn  34045  xrge0pluscn  34118  esumfzf  34247  esumiun  34272  volmeas  34409  omssubadd  34478  breprexplemc  34810  bnj553  35074  cvmliftlem6  35506  cvmliftlem10  35510  cvmlift2lem3  35521  finxpreclem4  37649  sin2h  37861  matunitlindflem2  37868  poimirlem16  37887  heibor  38072  ghomdiv  38143  3atlem1  39859  atmod3i2  40241  trljat2  40543  cdleme1  40603  cdleme22eALTN  40721  cdlemh2  41192  dihglblem3N  41671  dih1dimatlem0  41704  djhlsmcl  41790  mapdpglem30  42078  hdmapneg  42222  hgmapval1  42269  hgmapmul  42271  sn-1ne2  42635  sn-addrid  42791  fltnltalem  43020  3cubeslem3r  43044  3cubeslem4  43046  proot1ex  43553  tfsconcatfv  43698  dirkerper  46454  fourierdlem83  46547  fourierdlem92  46556  sigarperm  47218  sigaradd  47224  fmtnorec1  47897  lincresunit3lem2  48840  itsclc0yqsollem1  49122  itsclinecirc0b  49134  fuco11bALT  49697  prstchomval  49918  sinhpcosh  50099  amgmwlem  50161