Theorem 3eqtr2rd 2782

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

Syntax hints:   → wi 4   = wceq 1537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727

This theorem is referenced by:  nneob  8693  xp1d2m1eqxm1d2  12518  negmod  13954  modeqmodmin  13979  faclbnd2  14327  cats1un  14756  cjmulval  15181  fsumsplit  15774  fzosump1  15785  bcxmas  15868  trireciplem  15895  geo2sum  15906  geo2lim  15908  geoisum1c  15913  mertenslem1  15917  fprodsplit  15999  risefallfac  16057  bpolydiflem  16087  eftlub  16142  tanadd  16200  addsin  16203  subsin  16204  subcos  16208  sadadd2lem2  16484  qredeu  16692  zsqrtelqelz  16792  4sqlem15  16993  rcaninv  17842  resssetc  18146  resscatc  18163  estrreslem1OLD  18193  curfcl  18289  mulgaddcomlem  19128  conjghm  19280  gasubg  19333  dfod2  19597  efginvrel2  19760  efgcpbllemb  19788  odadd2  19882  frgpnabllem1  19906  srgbinomlem3  20246  pws1  20339  prdslmodd  20985  znunithash  21601  frlmipval  21817  frlmlbs  21835  psrlmod  21998  restcld  23196  clmneg  25128  rrxds  25441  itg2monolem1  25800  itgconst  25869  dvexp  26006  dvfsumabs  26078  dvtaylp  26427  taylthlem2  26431  taylthlem2OLD  26432  tangtx  26562  logsqrt  26761  zrtelqelz  26816  lawcoslem1  26873  chordthmlem2  26891  chordthmlem4  26893  tanatan  26977  atanbndlem  26983  amgmlem  27048  basellem3  27141  basellem5  27143  mpodvdsmulf1o  27252  dvdsmulf1o  27254  chtub  27271  fsumvma  27272  lgsquad2lem1  27443  2sqlem8  27485  dchrmusum2  27553  logsqvma  27601  pntrlog2bndlem4  27639  miriso  28693  lmieu  28807  ttgcontlem1  28914  brbtwn2  28935  ax5seglem1  28958  axcontlem2  28995  axcontlem4  28997  clwwlkel  30075  vc0  30603  hvsubdistr2  31079  adjlnop  32115  adjcoi  32129  cnvbraval  32139  fpwrelmap  32751  fsumiunle  32836  xrge0adddir  33006  cycpm2tr  33122  cycpmco2lem4  33132  cycpmco2lem7  33135  cyc3genpmlem  33154  archirngz  33179  archiabllem1b  33182  erler  33252  qusrn  33417  ressply10g  33572  ply1gsumz  33599  fedgmullem1  33657  fedgmullem2  33658  dimlssid  33660  constrrtcc  33741  rspectopn  33828  xrge0pluscn  33901  esumfzf  34050  esumiun  34075  volmeas  34212  omssubadd  34282  breprexplemc  34626  bnj553  34891  cvmliftlem6  35275  cvmliftlem10  35279  cvmlift2lem3  35290  finxpreclem4  37377  sin2h  37597  matunitlindflem2  37604  poimirlem16  37623  heibor  37808  ghomdiv  37879  3atlem1  39466  atmod3i2  39848  trljat2  40150  cdleme1  40210  cdleme22eALTN  40328  cdlemh2  40799  dihglblem3N  41278  dih1dimatlem0  41311  djhlsmcl  41397  mapdpglem30  41685  hdmapneg  41829  hgmapval1  41876  hgmapmul  41878  sn-1ne2  42279  sn-addrid  42427  fltnltalem  42649  3cubeslem3r  42675  3cubeslem4  42677  proot1ex  43185  tfsconcatfv  43331  dirkerper  46052  fourierdlem83  46145  fourierdlem92  46154  sigarperm  46816  sigaradd  46822  fmtnorec1  47462  lincresunit3lem2  48326  itsclc0yqsollem1  48612  itsclinecirc0b  48624  prstchomval  48875  sinhpcosh  48971  amgmwlem  49033