MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr2rd Structured version   Visualization version   GIF version

Theorem 3eqtr2rd 2650
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
StepHypRef Expression
1 3eqtr2d.1 . . 3 (𝜑𝐴 = 𝐵)
2 3eqtr2d.2 . . 3 (𝜑𝐶 = 𝐵)
31, 2eqtr4d 2646 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2644 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-cleq 2602
This theorem is referenced by:  nneob  7596  xp1d2m1eqxm1d2  11133  negmod  12532  modeqmodmin  12557  faclbnd2  12895  cats1un  13273  cjmulval  13679  fsumsplit  14264  fzosump1  14271  bcxmas  14352  trireciplem  14379  geo2sum  14389  geo2lim  14391  geoisum1c  14396  mertenslem1  14401  fprodsplit  14481  risefallfac  14540  bpolydiflem  14570  eftlub  14624  tanadd  14682  addsin  14685  subsin  14686  subcos  14690  sadadd2lem2  14956  qredeu  15156  zsqrtelqelz  15250  4sqlem15  15447  rcaninv  16223  resssetc  16511  resscatc  16524  estrreslem1  16546  curfcl  16641  mulgaddcomlem  17332  conjghm  17460  gasubg  17504  dfod2  17750  efginvrel2  17909  efgcpbllemb  17937  odadd2  18021  frgpnabllem1  18045  srgbinomlem3  18311  pws1  18385  prdslmodd  18736  psrlmod  19168  znunithash  19677  frlmipval  19879  frlmlbs  19897  restcld  20728  clmneg  22620  rrxds  22906  itg2monolem1  23240  itgconst  23308  dvexp  23439  dvfsumabs  23507  dvtaylp  23845  taylthlem2  23849  tangtx  23978  logsqrt  24167  lawcoslem1  24262  chordthmlem2  24277  chordthmlem4  24279  tanatan  24363  atanbndlem  24369  amgmlem  24433  basellem3  24526  basellem5  24528  dvdsmulf1o  24637  chtub  24654  fsumvma  24655  lgsquad2lem1  24826  2sqlem8  24868  dchrmusum2  24900  logsqvma  24948  pntrlog2bndlem4  24986  miriso  25283  lmieu  25394  sacgr  25440  ttgcontlem1  25483  brbtwn2  25503  ax5seglem1  25526  axcontlem2  25563  axcontlem4  25565  vc0  26590  hvsubdistr2  27097  adjlnop  28135  adjcoi  28149  cnvbraval  28159  fpwrelmap  28702  xrge0adddir  28829  archirngz  28880  archiabllem1b  28883  xrge0pluscn  29120  esumfzf  29264  esumiun  29289  volmeas  29427  omssubadd  29495  bnj553  30028  cvmliftlem6  30332  cvmliftlem10  30336  cvmlift2lem3  30347  finxpreclem4  32203  sin2h  32365  matunitlindflem2  32372  poimirlem16  32391  heibor  32586  ghomdiv  32657  3atlem1  33583  atmod3i2  33965  trljat2  34268  cdleme1  34328  cdleme22eALTN  34447  cdlemh2  34918  dihglblem3N  35398  dih1dimatlem0  35431  djhlsmcl  35517  mapdpglem30  35805  hdmapneg  35952  hgmapval1  35999  hgmapmul  36001  proot1ex  36594  dirkerper  38786  fourierdlem83  38879  fourierdlem92  38888  sigarperm  39495  sigaradd  39501  fmtnorec1  39785  lincresunit3lem2  42058  sinhpcosh  42236  amgmwlem  42313
  Copyright terms: Public domain W3C validator