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  8620  xp1d2m1eqxm1d2  12436  negmod  13881  modeqmodmin  13906  faclbnd2  14256  cats1un  14686  cjmulval  15111  fsumsplit  15707  fzosump1  15718  bcxmas  15801  trireciplem  15828  geo2sum  15839  geo2lim  15841  geoisum1c  15846  mertenslem1  15850  fprodsplit  15932  risefallfac  15990  bpolydiflem  16020  eftlub  16077  tanadd  16135  addsin  16138  subsin  16139  subcos  16143  sadadd2lem2  16420  qredeu  16628  zsqrtelqelz  16728  4sqlem15  16930  rcaninv  17756  resssetc  18054  resscatc  18071  curfcl  18193  mulgaddcomlem  19029  conjghm  19181  gasubg  19234  dfod2  19494  efginvrel2  19657  efgcpbllemb  19685  odadd2  19779  frgpnabllem1  19803  srgbinomlem3  20137  pws1  20234  prdslmodd  20875  znunithash  21474  frlmipval  21688  frlmlbs  21706  psrlmod  21869  restcld  23059  clmneg  24981  rrxds  25293  itg2monolem1  25651  itgconst  25720  dvexp  25857  dvfsumabs  25929  dvtaylp  26278  taylthlem2  26282  taylthlem2OLD  26283  tangtx  26414  logsqrt  26613  zrtelqelz  26668  lawcoslem1  26725  chordthmlem2  26743  chordthmlem4  26745  tanatan  26829  atanbndlem  26835  amgmlem  26900  basellem3  26993  basellem5  26995  mpodvdsmulf1o  27104  dvdsmulf1o  27106  chtub  27123  fsumvma  27124  lgsquad2lem1  27295  2sqlem8  27337  dchrmusum2  27405  logsqvma  27453  pntrlog2bndlem4  27491  pw2divsnegd  28332  miriso  28597  lmieu  28711  ttgcontlem1  28812  brbtwn2  28832  ax5seglem1  28855  axcontlem2  28892  axcontlem4  28894  clwwlkel  29975  vc0  30503  hvsubdistr2  30979  adjlnop  32015  adjcoi  32029  cnvbraval  32039  fpwrelmap  32656  fsumiunle  32754  xrge0adddir  32959  cycpm2tr  33076  cycpmco2lem4  33086  cycpmco2lem7  33089  cyc3genpmlem  33108  archirngz  33143  archiabllem1b  33146  erler  33216  qusrn  33380  ressply10g  33536  ply1gsumz  33564  fedgmullem1  33625  fedgmullem2  33626  dimlssid  33628  constrrtcc  33725  rspectopn  33857  xrge0pluscn  33930  esumfzf  34059  esumiun  34084  volmeas  34221  omssubadd  34291  breprexplemc  34623  bnj553  34888  cvmliftlem6  35277  cvmliftlem10  35281  cvmlift2lem3  35292  finxpreclem4  37382  sin2h  37604  matunitlindflem2  37611  poimirlem16  37630  heibor  37815  ghomdiv  37886  3atlem1  39477  atmod3i2  39859  trljat2  40161  cdleme1  40221  cdleme22eALTN  40339  cdlemh2  40810  dihglblem3N  41289  dih1dimatlem0  41322  djhlsmcl  41408  mapdpglem30  41696  hdmapneg  41840  hgmapval1  41887  hgmapmul  41889  sn-1ne2  42253  sn-addrid  42409  fltnltalem  42650  3cubeslem3r  42675  3cubeslem4  42677  proot1ex  43185  tfsconcatfv  43330  dirkerper  46094  fourierdlem83  46187  fourierdlem92  46196  sigarperm  46858  sigaradd  46864  fmtnorec1  47538  lincresunit3lem2  48469  itsclc0yqsollem1  48751  itsclinecirc0b  48763  fuco11bALT  49327  prstchomval  49548  sinhpcosh  49729  amgmwlem  49791