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

Theorem 3eqtr2rd 2692
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 2688 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2686 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  nneob  7777  xp1d2m1eqxm1d2  11324  negmod  12755  modeqmodmin  12780  faclbnd2  13118  cats1un  13521  cjmulval  13929  fsumsplit  14515  fzosump1  14525  bcxmas  14611  trireciplem  14638  geo2sum  14648  geo2lim  14650  geoisum1c  14655  mertenslem1  14660  fprodsplit  14740  risefallfac  14799  bpolydiflem  14829  eftlub  14883  tanadd  14941  addsin  14944  subsin  14945  subcos  14949  sadadd2lem2  15219  qredeu  15419  zsqrtelqelz  15513  4sqlem15  15710  rcaninv  16501  resssetc  16789  resscatc  16802  estrreslem1  16824  curfcl  16919  mulgaddcomlem  17610  conjghm  17738  gasubg  17781  dfod2  18027  efginvrel2  18186  efgcpbllemb  18214  odadd2  18298  frgpnabllem1  18322  srgbinomlem3  18588  pws1  18662  prdslmodd  19017  psrlmod  19449  znunithash  19961  frlmipval  20166  frlmlbs  20184  restcld  21024  clmneg  22927  rrxds  23227  itg2monolem1  23562  itgconst  23630  dvexp  23761  dvfsumabs  23831  dvtaylp  24169  taylthlem2  24173  tangtx  24302  logsqrt  24495  lawcoslem1  24590  chordthmlem2  24605  chordthmlem4  24607  tanatan  24691  atanbndlem  24697  amgmlem  24761  basellem3  24854  basellem5  24856  dvdsmulf1o  24965  chtub  24982  fsumvma  24983  lgsquad2lem1  25154  2sqlem8  25196  dchrmusum2  25228  logsqvma  25276  pntrlog2bndlem4  25314  miriso  25610  lmieu  25721  sacgr  25767  ttgcontlem1  25810  brbtwn2  25830  ax5seglem1  25853  axcontlem2  25890  axcontlem4  25892  vc0  27557  hvsubdistr2  28035  adjlnop  29073  adjcoi  29087  cnvbraval  29097  fpwrelmap  29636  fsumiunle  29703  xrge0adddir  29820  archirngz  29871  archiabllem1b  29874  xrge0pluscn  30114  esumfzf  30259  esumiun  30284  volmeas  30422  omssubadd  30490  breprexplemc  30838  bnj553  31094  cvmliftlem6  31398  cvmliftlem10  31402  cvmlift2lem3  31413  finxpreclem4  33361  sin2h  33529  matunitlindflem2  33536  poimirlem16  33555  heibor  33750  ghomdiv  33821  3atlem1  35087  atmod3i2  35469  trljat2  35772  cdleme1  35832  cdleme22eALTN  35950  cdlemh2  36421  dihglblem3N  36901  dih1dimatlem0  36934  djhlsmcl  37020  mapdpglem30  37308  hdmapneg  37455  hgmapval1  37502  hgmapmul  37504  proot1ex  38096  dirkerper  40631  fourierdlem83  40724  fourierdlem92  40733  sigarperm  41370  sigaradd  41376  fmtnorec1  41774  lincresunit3lem2  42594  sinhpcosh  42809  amgmwlem  42876
  Copyright terms: Public domain W3C validator