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

Theorem 3eqtr2rd 2799
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 2795 . 2 (𝜑𝐴 = 𝐶)
4 3eqtr2d.3 . 2 (𝜑𝐶 = 𝐷)
53, 4eqtr2d 2793 1 (𝜑𝐷 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1852  df-cleq 2751
This theorem is referenced by:  nneob  7899  xp1d2m1eqxm1d2  11476  negmod  12907  modeqmodmin  12932  faclbnd2  13270  cats1un  13673  cjmulval  14082  fsumsplit  14668  fzosump1  14678  bcxmas  14764  trireciplem  14791  geo2sum  14801  geo2lim  14803  geoisum1c  14808  mertenslem1  14813  fprodsplit  14893  risefallfac  14952  bpolydiflem  14982  eftlub  15036  tanadd  15094  addsin  15097  subsin  15098  subcos  15102  sadadd2lem2  15372  qredeu  15572  zsqrtelqelz  15666  4sqlem15  15863  rcaninv  16653  resssetc  16941  resscatc  16954  estrreslem1  16976  curfcl  17071  mulgaddcomlem  17762  conjghm  17890  gasubg  17933  dfod2  18179  efginvrel2  18338  efgcpbllemb  18366  odadd2  18450  frgpnabllem1  18474  srgbinomlem3  18740  pws1  18814  prdslmodd  19169  psrlmod  19601  znunithash  20113  frlmipval  20318  frlmlbs  20336  restcld  21176  clmneg  23079  rrxds  23379  itg2monolem1  23714  itgconst  23782  dvexp  23913  dvfsumabs  23983  dvtaylp  24321  taylthlem2  24325  tangtx  24454  logsqrt  24647  lawcoslem1  24742  chordthmlem2  24757  chordthmlem4  24759  tanatan  24843  atanbndlem  24849  amgmlem  24913  basellem3  25006  basellem5  25008  dvdsmulf1o  25117  chtub  25134  fsumvma  25135  lgsquad2lem1  25306  2sqlem8  25348  dchrmusum2  25380  logsqvma  25428  pntrlog2bndlem4  25466  miriso  25762  lmieu  25873  sacgr  25919  ttgcontlem1  25962  brbtwn2  25982  ax5seglem1  26005  axcontlem2  26042  axcontlem4  26044  vc0  27736  hvsubdistr2  28214  adjlnop  29252  adjcoi  29266  cnvbraval  29276  fpwrelmap  29815  fsumiunle  29882  xrge0adddir  29999  archirngz  30050  archiabllem1b  30053  xrge0pluscn  30293  esumfzf  30438  esumiun  30463  volmeas  30601  omssubadd  30669  breprexplemc  31017  bnj553  31273  cvmliftlem6  31577  cvmliftlem10  31581  cvmlift2lem3  31592  finxpreclem4  33540  sin2h  33710  matunitlindflem2  33717  poimirlem16  33736  heibor  33931  ghomdiv  34002  3atlem1  35270  atmod3i2  35652  trljat2  35955  cdleme1  36015  cdleme22eALTN  36133  cdlemh2  36604  dihglblem3N  37084  dih1dimatlem0  37117  djhlsmcl  37203  mapdpglem30  37491  hdmapneg  37638  hgmapval1  37685  hgmapmul  37687  proot1ex  38279  dirkerper  40814  fourierdlem83  40907  fourierdlem92  40916  sigarperm  41553  sigaradd  41559  fmtnorec1  41957  lincresunit3lem2  42777  sinhpcosh  42992  amgmwlem  43059
  Copyright terms: Public domain W3C validator